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

end;

let k be Element of 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 number ; :: thesis:
assume p > 0 ; :: thesis:
then consider n being Element of NAT such that
A6: for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj (k,z,w)).||) . k) < p by Th31;
take n = n; :: thesis:

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

end;

hence for k being Element of NAT st n <= k holds
abs ((rseq . k) - 0) < p ; :: thesis:

end;