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

proof

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;

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