theorem Th9: :: REAL_NS3:9

for x being real-valued FinSequence holds 0 <= Sum (abs x)