let seq, cseq be Complex_Sequence; :: thesis: ( cseq = <i> (#) seq implies ( seq is convergent_to_0 iff cseq is convergent_to_0 ) )
assume A1: cseq = <i> (#) seq ; :: 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 A2: seq is convergent_to_0 ; :: thesis: cseq is convergent_to_0
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-empty & <i> (#) seq is convergent ) by A2, COMSEQ_1:38, COMSEQ_2:17;
hence cseq is convergent_to_0 by A1, A3, CFDIFF_1:def 1; :: thesis: verum

end;

assume A4: cseq is convergent_to_0 ; :: thesis: seq is convergent_to_0
then A5: seq is non-empty by A1, Lm5;
(- <i>) (#) (<i> (#) seq) is convergent by A1, A4, COMSEQ_2:17;
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 convergent_to_0 by A6, A5, CFDIFF_1:def 1; :: thesis: verum