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

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

deffunc H1( Nat) -> Element of REAL = (Partial_Sums ||.(Conj (\$1,z,w)).||) . \$1;
ex rseq being Real_Sequence st
for k being Nat holds rseq . k = H1(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: ( ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0. X ) )
assume A2: for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; :: thesis: ( seq is convergent & lim seq = 0. X )
A3: now :: thesis: for k being Nat holds ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k
let k be Nat; :: thesis: ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k
||.(seq . k).|| = ||.((Partial_Sums (Conj (k,z,w))) . k).|| by A2;
hence ||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by Th10; :: thesis: verum
end;
A4: now :: thesis: for k being Nat holds ||.(seq . k).|| <= rseq . k
let k be Nat; :: thesis: ||.(seq . k).|| <= rseq . k
||.(seq . k).|| <= (Partial_Sums ||.(Conj (k,z,w)).||) . k by A3;
hence ||.(seq . k).|| <= rseq . k by A1; :: thesis: verum
end;
A5: now :: thesis: for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.((rseq . k) - 0).| < p
let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for k being Nat st n <= k holds
|.((rseq . k) - 0).| < p )

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

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: for k being Nat st n <= k holds
|.((rseq . k) - 0).| < p

now :: thesis: for k being Nat st n <= k holds
|.((rseq . k) - 0).| < p
let k be Nat; :: thesis: ( n <= k implies |.((rseq . k) - 0).| < p )
assume A7: n <= k ; :: thesis: |.((rseq . k) - 0).| < p
|.((rseq . k) - 0).| = |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| by A1;
hence |.((rseq . k) - 0).| < p by A6, A7; :: thesis: verum
end;
hence for k being Nat st n <= k holds
|.((rseq . k) - 0).| < p ; :: thesis: verum
end;
then A8: rseq is convergent by SEQ_2:def 6;
then lim rseq = 0 by ;
hence ( seq is convergent & lim seq = 0. X ) by A4, A8, Th12; :: thesis: verum