let seq be Complex_Sequence; :: thesis: ( seq is non-zero implies |.seq.| is non-zero )
assume A1: seq is non-zero ; :: thesis: |.seq.| is non-zero

now

let n be Element of NAT ; :: thesis: |.seq.| . n <> 0
seq . n <> 0c by A1, Th4;
then |.(seq . n).| <> 0 by COMPLEX1:45;
hence |.seq.| . n <> 0 by VALUED_1:18; :: thesis: verum

end;

hence |.seq.| is non-zero by SEQ_1:5; :: thesis: verum