let rseq be Real_Sequence; :: thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds
( seq is convergent & lim seq = 0c )
let seq be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0c ) )
assume A1: ( ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 ) ; :: thesis: ( seq is convergent & lim seq = 0c )
C . 0 = 0 by FUNCOP_1:13;
then A2: ( C is convergent & lim C = 0 ) by SEQ_4:40;
A3: ( ( for n being Element of NAT holds C . n <= (abs (Re seq)) . n ) & ( for n being Element of NAT holds (abs (Re seq)) . n <= rseq . n ) )

proof

A4: now

let n be Element of NAT ; :: thesis: C . n <= (abs (Re seq)) . n
0 <= (abs (Re seq)) . n

proof

(abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:16;
hence 0 <= (abs (Re seq)) . n by COMPLEX1:132; :: thesis: verum

end;

hence C . n <= (abs (Re seq)) . n by FUNCOP_1:13; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (abs (Re seq)) . n <= rseq . n
(Re seq) . n = Re (seq . n) by Def3;
then A5: (abs (Re seq)) . n = abs (Re (seq . n)) by SEQ_1:16;
A6: abs (Re (seq . n)) <= |.(seq . n).| by Th13;
|.(seq . n).| <= rseq . n by A1;
hence (abs (Re seq)) . n <= rseq . n by A5, A6, XXREAL_0:2; :: thesis: verum

end;

hence ( ( for n being Element of NAT holds C . n <= (abs (Re seq)) . n ) & ( for n being Element of NAT holds (abs (Re seq)) . n <= rseq . n ) ) by A4; :: thesis: verum

end;

A7: ( ( for n being Element of NAT holds C . n <= (abs (Im seq)) . n ) & ( for n being Element of NAT holds (abs (Im seq)) . n <= rseq . n ) )

proof

A8: now

let n be Element of NAT ; :: thesis: C . n <= (abs (Im seq)) . n
0 <= (abs (Im seq)) . n

proof

(abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:16;
hence 0 <= (abs (Im seq)) . n by COMPLEX1:132; :: thesis: verum

end;

hence C . n <= (abs (Im seq)) . n by FUNCOP_1:13; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (abs (Im seq)) . n <= rseq . n
A9: (Im seq) . n = Im (seq . n) by Def4;
A10: (abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:16;
A11: abs (Im (seq . n)) <= |.(seq . n).| by Th13;
|.(seq . n).| <= rseq . n by A1;
hence (abs (Im seq)) . n <= rseq . n by A9, A10, A11, XXREAL_0:2; :: thesis: verum

end;

hence ( ( for n being Element of NAT holds C . n <= (abs (Im seq)) . n ) & ( for n being Element of NAT holds (abs (Im seq)) . n <= rseq . n ) ) by A8; :: thesis: verum

end;

A12: abs (Re seq) is convergent by A1, A2, A3, SEQ_2:33;
A13: lim (abs (Re seq)) = 0 by A1, A2, A3, SEQ_2:34;
A14: abs (Im seq) is convergent by A1, A2, A7, SEQ_2:33;
A15: lim (abs (Im seq)) = 0 by A1, A2, A7, SEQ_2:34;
A16: ( Re seq is convergent & lim (Re seq) = 0 ) by A12, A13, SEQ_4:28;
( Im seq is convergent & lim (Im seq) = 0 ) by A14, A15, SEQ_4:28;
then ( seq is convergent & Re (lim seq) = 0 & Im (lim seq) = 0 ) by A16, Th42;
hence ( seq is convergent & lim seq = 0c ) by Lm1, COMPLEX1:29; :: thesis: verum