theorem Th9: :: TOPREAL7:9

for f being FinSequence of REAL holds
( len f = len (abs f) & dom f = dom (abs f) )