let seq be Real_Sequence; :: thesis: ( seq is non-zero implies abs seq is non-zero )
assume A1: seq is non-zero ; :: thesis: abs seq is non-zero

now

let n be Element of NAT ; :: thesis: (abs seq) . n <> 0
seq . n <> 0 by A1, Th7;
then abs (seq . n) <> 0 by COMPLEX1:47;
hence (abs seq) . n <> 0 by Th16; :: thesis: verum

end;

hence abs seq is non-zero by Th7; :: thesis: verum