Positive Definite Sequence of Operators and a Fixed Point Theorem

The purpose of this note is to prove the following:Theorem. Let {An} be a positive definite sequence of operators on a Hilbert space H with A0=1. If A1f=f for some f in H, then Anf=f for all n.Note that a bilateral sequence of operators {An:n = 0, ±1, ±2,…} on H is positive definite iffor every finitely nonzero sequence {fn} of vectors in H [1].