let seq, cseq be Complex_Sequence; :: thesis: ( cseq = <i> (#) seq implies ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) ) )

assume A1: cseq = <i> (#) seq ; :: 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 A5: seq is non-zero by A1, Lm4;

(- <i>) (#) (<i> (#) seq) is convergent by A1, A4;

then ((- <i>) * <i>) (#) seq is convergent by CFUNCT_1:22;

then A6: seq is convergent by CFUNCT_1:26;

lim (<i> (#) seq) = 0 by A1, A4, CFDIFF_1:def 1;

then <i> * (lim seq) = 0 by A6, COMSEQ_2:18;

hence ( seq is 0 -convergent & seq is non-zero ) by A6, A5, CFDIFF_1:def 1; :: thesis: verum

assume A1: cseq = <i> (#) seq ; :: 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 A4:
( 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 lim seq = 0 by CFDIFF_1:def 1;

then A3: lim (<i> (#) seq) = <i> * 0 by A2, COMSEQ_2:18

.= 0 ;

( <i> (#) seq is non-zero & <i> (#) seq is convergent ) by A2, COMSEQ_1:38;

hence ( cseq is 0 -convergent & cseq is non-zero ) by A1, A3, CFDIFF_1:def 1; :: thesis: verum

end;then lim seq = 0 by CFDIFF_1:def 1;

then A3: lim (<i> (#) seq) = <i> * 0 by A2, COMSEQ_2:18

.= 0 ;

( <i> (#) seq is non-zero & <i> (#) seq is convergent ) by A2, COMSEQ_1:38;

hence ( cseq is 0 -convergent & cseq is non-zero ) by A1, A3, CFDIFF_1:def 1; :: thesis: verum

then A5: seq is non-zero by A1, Lm4;

(- <i>) (#) (<i> (#) seq) is convergent by A1, A4;

then ((- <i>) * <i>) (#) seq is convergent by CFUNCT_1:22;

then A6: seq is convergent by CFUNCT_1:26;

lim (<i> (#) seq) = 0 by A1, A4, CFDIFF_1:def 1;

then <i> * (lim seq) = 0 by A6, COMSEQ_2:18;

hence ( seq is 0 -convergent & seq is non-zero ) by A6, A5, CFDIFF_1:def 1; :: thesis: verum