theorem Th12: :: SEQ_1:12

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