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 ) )

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

( 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 A6:
( cseq is 0 -convergent & cseq is non-zero )
; :: thesis: ( seq is 0 -convergent & seq is non-zero )
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;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

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