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

proof

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

now

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-empty by COMSEQ_1:4; :: thesis: verum

end;

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