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 that
A1: for n being Element of NAT holds |.(seq . n).| <= rseq . n and
A2: ( rseq is convergent & lim rseq = 0 ) ; :: thesis: ( seq is convergent & lim seq = 0c )

A3: now

let n be Element of NAT ; :: thesis: C . n <= (abs (Re seq)) . n
(abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12;
then 0 <= (abs (Re seq)) . n by COMPLEX1:46;
hence C . n <= (abs (Re seq)) . n by FUNCOP_1:7; :: thesis: verum

end;

C . 0 = 0 by FUNCOP_1:7;
then A4: lim C = 0 by SEQ_4:25;

now

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

end;

then A6: ( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 ) by A2, A4, A3, SEQ_2:19, SEQ_2:20;
then A7: Re seq is convergent by SEQ_4:15;

A8: now

let n be Element of NAT ; :: thesis: C . n <= (abs (Im seq)) . n
(abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:12;
then 0 <= (abs (Im seq)) . n by COMPLEX1:46;
hence C . n <= (abs (Im seq)) . n by FUNCOP_1:7; :: thesis: verum

end;

now

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

end;

then A10: ( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 ) by A2, A4, A8, SEQ_2:19, SEQ_2:20;
then A11: Im seq is convergent by SEQ_4:15;
lim (Im seq) = 0 by A10, SEQ_4:15;
then A12: Im (lim seq) = 0 by A7, A11, Th42;
lim (Re seq) = 0 by A6, SEQ_4:15;
then Re (lim seq) = 0 by A7, A11, Th42;
hence ( seq is convergent & lim seq = 0c ) by A7, A11, A12, Lm1, Th42, COMPLEX1:13; :: thesis: verum