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 seq is convergent_to_0 ; :: thesis: cseq is convergent_to_0
then ( seq is non-zero & seq is convergent & lim seq = 0 ) by FDIFF_1:def 1;
then ( cseq is non-zero & cseq is convergent & lim cseq = 0 ) by A1, LM03, LM05;
hence cseq is convergent_to_0 by CFDIFF_1:def 1; :: thesis: verum

end;

assume A3a: cseq is convergent_to_0 ; :: thesis: seq is convergent_to_0
then A3: ( cseq is non-zero & cseq is convergent & lim cseq = 0 ) by CFDIFF_1:def 1;
A4: seq is convergent by A1, LM03, A3a;
lim seq = 0 by A1, A3, LM06;
hence seq is convergent_to_0 by A1, A3a, A4, FDIFF_1:def 1; :: thesis: verum