for seq, seq1 being Real_Sequence holds
( seq1 = abs seq iff for n being Nat holds seq1 . n = |.(seq . n).| )