let z, w be Element of COMPLEX ; :: thesis: for seq being Complex_Sequence st ( for k being Element of 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 Element of NAT holds seq . k = (Partial_Sums (Conj k,z,w)) . k ) implies ( seq is convergent & lim seq = 0 ) )

now

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

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

A7: now

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

end;

A9: 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
A11: for k being Element of NAT st n <= k holds
abs ((Partial_Sums |.(Conj k,z,w).|) . k) < p by Th22;
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 A13: n <= k ; :: thesis: abs ((rseq . k) - 0 ) < p
abs ((rseq . k) - 0 ) = abs ((Partial_Sums |.(Conj k,z,w).|) . k) by A6;
hence abs ((rseq . k) - 0 ) < p by A11, A13; :: thesis: verum

end;

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

end;

then A15: rseq is convergent by SEQ_2:def 6;
then lim rseq = 0 by A9, SEQ_2:def 7;
hence ( seq is convergent & lim seq = 0c ) by A7, A15, COMSEQ_3:48; :: thesis: verum

end;

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