let w, z be Complex; :: thesis:
let seq be Complex_Sequence; :: thesis:

let seq be Complex_Sequence; :: thesis:
assume A1: for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ; :: thesis:

A2: now :: thesis:

let k be Nat; :: thesis:
|.(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:

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:

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

end;

A5: now :: thesis:

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 Th21;
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 A3;
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;

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:

end;

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