let seq, cseq be Complex_Sequence; :: thesis: ( cseq = <i> (#) seq implies ( seq is non-zero iff cseq is non-zero ) )
assume A1: cseq = <i> (#) seq ; :: thesis: ( seq is non-zero iff cseq is non-zero )
thus ( seq is non-zero implies cseq is non-zero ) by A1, COMSEQ_1:38; :: thesis: ( cseq is non-zero implies seq is non-zero )
A2: ( <i> (#) seq is non-zero implies seq is non-zero )

proof

assume A3: <i> (#) seq is non-zero ; :: thesis: seq is non-zero

now :: thesis: for n being Element of NAT holds seq . n <> 0c

let n be Element of NAT ; :: thesis: seq . n <> 0c
(<i> (#) seq) . n <> 0c by A3, COMSEQ_1:4;
then <i> * (seq . n) <> 0c by VALUED_1:6;
hence seq . n <> 0c ; :: thesis: verum

end;

hence seq is non-zero by COMSEQ_1:4; :: thesis: verum

end;

assume cseq is non-zero ; :: thesis: seq is non-zero
hence seq is non-zero by A1, A2; :: thesis: verum