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

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

end;

deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums |.(Conj $1,z,w).|) . $1;
A5: ex rseq being Real_Sequence st
for k being Element of NAT holds rseq . k = H₁(k) from SEQ_1:sch 1();
consider rseq being Real_Sequence such that
A6: for k being Element of NAT holds rseq . k = (Partial_Sums |.(Conj k,z,w).|) . k by A5;

A7: now

let k be Element of NAT ; :: thesis: |.(seq . k).| <= rseq . k
A8: |.(seq . k).| <= (Partial_Sums |.(Conj k,z,w).|) . k by A3;
thus |.(seq . k).| <= rseq . k by A6, A8; :: 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 A10: 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
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 A10, Th22;
take n = n; :: thesis: for k being Element of NAT st n <= k holds
abs ((rseq . k) - 0 ) < p

A12: 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
A14: abs ((rseq . k) - 0 ) = abs ((Partial_Sums |.(Conj k,z,w).|) . k) by A6;
thus abs ((rseq . k) - 0 ) < p by A11, A13, A14; :: thesis: verum

end;

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

end;

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

end;

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