theorem Th6: :: EUCLID:9

for f being real-valued FinSequence holds |.f.| >= 0