theorem Th86: :: RVSUM_1:86

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