let rseq be Real_Sequence; :: thesis: for seq being Complex_Sequence st ( for n being 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 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 Nat holds |.(seq . n).| <= rseq . n and
A2: ( rseq is convergent & lim rseq = 0 ) ; :: thesis: ( seq is convergent & lim seq = 0c )

A3: now :: thesis: for n being Nat holds (seq_const 0) . n <= (abs (Re seq)) . n

let n be Nat; :: thesis: (seq_const 0) . n <= (abs (Re seq)) . n
(abs (Re seq)) . n = |.((Re seq) . n).| by SEQ_1:12;
then 0 <= (abs (Re seq)) . n by COMPLEX1:46;
hence (seq_const 0) . n <= (abs (Re seq)) . n ; :: thesis: verum

end;

(seq_const 0) . 0 = 0 ;
then A4: lim (seq_const 0) = 0 by SEQ_4:25;

now :: thesis: for n being Nat holds (abs (Re seq)) . n <= rseq . n

let n be Nat; :: thesis: (abs (Re seq)) . n <= rseq . n
(Re seq) . n = Re (seq . n) by Def5;
then A5: (abs (Re seq)) . n = |.(Re (seq . n)).| by SEQ_1:12;
( |.(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 :: thesis: for n being Nat holds (seq_const 0) . n <= (abs (Im seq)) . n

let n be Nat; :: thesis: (seq_const 0) . n <= (abs (Im seq)) . n
(abs (Im seq)) . n = |.((Im seq) . n).| by SEQ_1:12;
then 0 <= (abs (Im seq)) . n by COMPLEX1:46;
hence (seq_const 0) . n <= (abs (Im seq)) . n ; :: thesis: verum

end;

now :: thesis: for n being Nat holds (abs (Im seq)) . n <= rseq . n

let n be Nat; :: thesis: (abs (Im seq)) . n <= rseq . n
A9: ( (Im seq) . n = Im (seq . n) & (abs (Im seq)) . n = |.((Im seq) . n).| ) by Def6, SEQ_1:12;
( |.(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