let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X
for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj k,z,w)) . k ) holds
( seq is convergent & lim seq = 0. X )
let z, w be Element of X; :: thesis: for seq being sequence of X st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj k,z,w)) . k ) holds
( seq is convergent & lim seq = 0. X )
let seq be sequence of X; :: thesis: ( ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj k,z,w)) . k ) implies ( seq is convergent & lim seq = 0. X ) )
assume A1: for k being Element of NAT holds seq . k = (Partial_Sums (Conj k,z,w)) . k ; :: thesis: ( seq is convergent & lim seq = 0. X )

A2: now

let k be Element of NAT ; :: thesis: ||.(seq . k).|| <= (Partial_Sums ||.(Conj k,z,w).||) . k
||.(seq . k).|| = ||.((Partial_Sums (Conj k,z,w)) . k).|| by A1;
hence ||.(seq . k).|| <= (Partial_Sums ||.(Conj k,z,w).||) . k by Th10; :: thesis: verum

end;

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
A3: for k being Element of NAT holds rseq . k = (Partial_Sums ||.(Conj k,z,w).||) . k ;

A4: now

let k be Element of NAT ; :: thesis: ||.(seq . k).|| <= rseq . k
||.(seq . k).|| <= (Partial_Sums ||.(Conj k,z,w).||) . k by A2;
hence ||.(seq . k).|| <= rseq . k by A3; :: thesis: verum

end;

( rseq is convergent & lim rseq = 0 )

proof

A5: now

let p be real number ; :: thesis: ( p > 0 implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((rseq . k) - 0 ) < p )
assume p > 0 ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((rseq . k) - 0 ) < p
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: for k being Element of NAT st n <= k holds
abs ((rseq . k) - 0 ) < p

now

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

end;

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

end;

hence rseq is convergent by SEQ_2:def 6; :: thesis: lim rseq = 0
hence lim rseq = 0 by A5, SEQ_2:def 7; :: thesis: verum

end;

hence ( seq is convergent & lim seq = 0. X ) by A4, Th12; :: thesis: verum