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