let X be Complex_Banach_Algebra; :: thesis:
let w, z be Element of X; :: thesis:
deffunc H₁( Nat) -> Element of REAL = (Partial_Sums ||.(Conj ($1,z,w)).||) . $1;
ex rseq being Real_Sequence st
for k being Nat holds rseq . k = H₁(k) from SEQ_1:sch 1();
then consider rseq being Real_Sequence such that
A1: for k being Nat holds rseq . k = (Partial_Sums ||.(Conj (k,z,w)).||) . k ;
let seq be sequence of X; :: thesis:
assume A2: for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; :: thesis:

end;

let k be Nat; :: thesis:
||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by A3;
hence ||.(seq . k).|| <= rseq . k by A1; :: thesis:

end;

let p be Real; :: thesis:
assume p > 0 ; :: thesis:
then consider n being Nat such that
A6: for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p by Th31;
take n = n; :: thesis:

let k be Nat; :: thesis:
assume A7: n <= k ; :: thesis:
|.((rseq . k) - 0).| = |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| by A1;
hence |.((rseq . k) - 0).| < p by A6, A7; :: thesis:

end;

hence for k being Nat st n <= k holds
|.((rseq . k) - 0).| < p ; :: thesis:

end;