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

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

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

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