for F being real-valued FinSequence holds 0 <= Sum (sqr F)