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
.= 0 ;
( <i> (#) seq is non-zero & <i> (#) seq is convergent ) by ;
hence ( cseq is 0 -convergent & cseq is non-zero ) by ; :: 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 ;
(- <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 ;
then <i> * (lim seq) = 0 by ;
hence ( seq is 0 -convergent & seq is non-zero ) by ; :: thesis: verum