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 A02: seq is convergent_to_0 ; :: thesis: cseq is convergent_to_0
then A2: ( seq is non-zero & seq is convergent & lim seq = 0 ) by CFDIFF_1:def 1;
A3: ( <i> (#) seq is non-zero & <i> (#) seq is convergent ) by A02, COMSEQ_1:41, COMSEQ_2:17;
lim (<i> (#) seq) = <i> * 0 by A2, COMSEQ_2:18
.= 0 ;
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
(- <i> ) (#) (<i> (#) seq) is convergent by A4, A1, COMSEQ_2:17;
then ((- <i> ) * <i> ) (#) seq is convergent by CFUNCT_1:31;
then A5: seq is convergent by CFUNCT_1:35;
A6: seq is non-zero by A1, A4, LM10;
lim (<i> (#) seq) = 0 by A1, A4, CFDIFF_1:def 1;
then <i> * (lim seq) = 0 by A5, COMSEQ_2:18;
hence seq is convergent_to_0 by A5, A6, CFDIFF_1:def 1; :: thesis: verum