theorem Th11: :: TOPREAL6:12

for a being Real
for i being Nat
for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds
(abs F) . i = |.a.|