let seq be Real_Sequence; :: thesis: for cseq being Complex_Sequence st seq = cseq holds
( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
let cseq be Complex_Sequence; :: thesis: ( seq = cseq implies ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) ) )
assume A1: seq = cseq ; :: thesis: ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
thus ( seq is 0 -convergent & seq is non-zero implies ( cseq is 0 -convergent & cseq is non-zero ) ) :: thesis: ( cseq is 0 -convergent & cseq is non-zero implies ( seq is 0 -convergent & seq is non-zero ) )

proof

assume A2: ( seq is 0 -convergent & seq is non-zero ) ; :: thesis: ( cseq is 0 -convergent & cseq is non-zero )
then A3: seq is convergent ;
lim seq = 0 by A2;
then A4: lim cseq = 0 by A1, A3, Lm1;
A5: cseq is non-zero by A1, A2;
cseq is convergent by A1, A3;
hence ( cseq is 0 -convergent & cseq is non-zero ) by A5, A4, CFDIFF_1:def 1; :: thesis: verum

end;

assume A6: ( cseq is 0 -convergent & cseq is non-zero ) ; :: thesis: ( seq is 0 -convergent & seq is non-zero )
then lim cseq = 0 by CFDIFF_1:def 1;
then A7: lim seq = 0 by A1, A6, Lm2;
thus ( seq is 0 -convergent & seq is non-zero ) by A1, A6, A7, FDIFF_1:def 1; :: thesis: verum