let seq be Real_Sequence; :: thesis: for cseq being Complex_Sequence st seq = cseq holds
( seq is convergent_to_0 iff cseq is convergent_to_0 )
let cseq be Complex_Sequence; :: thesis: ( seq = cseq implies ( seq is convergent_to_0 iff cseq is convergent_to_0 ) )
assume A1: seq = cseq ; :: thesis: ( seq is convergent_to_0 iff cseq is convergent_to_0 )
thus ( seq is convergent_to_0 implies cseq is convergent_to_0 ) :: thesis: ( cseq is convergent_to_0 implies seq is convergent_to_0 )

proof

assume A2: seq is convergent_to_0 ; :: thesis: cseq is convergent_to_0
then A3: seq is convergent by FDIFF_1:def 1;
lim seq = 0 by A2, FDIFF_1:def 1;
then A4: lim cseq = 0 by A1, A3, Lm2;
A5: cseq is non-empty by A1, A2, FDIFF_1:def 1;
cseq is convergent by A1, A3, Lm1;
hence cseq is convergent_to_0 by A5, A4, CFDIFF_1:def 1; :: thesis: verum

end;

assume A6: cseq is convergent_to_0 ; :: thesis: seq is convergent_to_0
then lim cseq = 0 by CFDIFF_1:def 1;
then A7: lim seq = 0 by A1, A6, Lm3;
seq is convergent by A1, A6, Lm1;
hence seq is convergent_to_0 by A1, A6, A7, FDIFF_1:def 1; :: thesis: verum