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 )
A3: ( <i> (#) seq is non-zero implies seq is non-zero )

proof

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

now

let n be Element of NAT ; :: thesis: seq . n <> 0c
(<i> (#) seq) . n <> 0c by A4, 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;

thus ( seq is non-zero implies cseq is non-zero ) by COMSEQ_1:41, A1; :: thesis: ( cseq is non-zero implies seq is non-zero )
assume cseq is non-zero ; :: thesis: seq is non-zero
hence seq is non-zero by A1, A3; :: thesis: verum