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

assume A1: seq is non-zero ; :: thesis: abs seq is non-zero

now :: thesis: for n being Nat holds (abs seq) . n <> 0

hence
abs seq is non-zero
by Th5; :: thesis: verumlet 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;seq . n <> 0 by A1, Th5;

then |.(seq . n).| <> 0 by COMPLEX1:47;

hence (abs seq) . n <> 0 by Th12; :: thesis: verum