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 )

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

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
cseq is non-zero
; :: thesis: seq is non-zero
assume A3:
<i> (#) seq is non-zero
; :: thesis: seq is non-zero

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

hence
seq is non-zero
by COMSEQ_1:4; :: thesis: verumlet 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;(<i> (#) seq) . n <> 0c by A3, COMSEQ_1:4;

then <i> * (seq . n) <> 0c by VALUED_1:6;

hence seq . n <> 0c ; :: thesis: verum

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