let w, z be Complex; :: thesis: for seq being Complex_Sequence st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds
( seq is convergent & lim seq = 0 )
let seq be Complex_Sequence; :: thesis: ( ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0 ) )

now :: thesis: for seq being Complex_Sequence st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds
( seq is convergent & lim seq = 0c )

let seq be Complex_Sequence; :: thesis: ( ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0c ) )
assume A1: for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; :: thesis: ( seq is convergent & lim seq = 0c )

A2: 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 A1;
hence |.(seq . k).| <= (Partial_Sums |.(Conj (k,z,w)).|) . k by COMSEQ_3:30; :: thesis: verum

end;

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

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 A2;
hence |.(seq . k).| <= rseq . k by A3; :: 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 Th21;
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 A3;
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 A5, SEQ_2:def 7;
hence ( seq is convergent & lim seq = 0c ) by A4, A8, COMSEQ_3:48; :: thesis: verum

end;

hence ( ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) implies ( seq is convergent & lim seq = 0 ) ) ; :: thesis: verum