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 :: thesis: for n being Nat holds (abs seq) . n <> 0

let n be Nat; :: thesis: (abs seq) . n <> 0
seq . n <> 0 by A1, Th5;
then |.(seq . n).| <> 0 by COMPLEX1:47;
hence (abs seq) . n <> 0 by Th12; :: thesis: verum

end;

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