theorem Th5: :: MATRTOP1:5

for rf being real-valued FinSequence st rf is nonnegative-yielding holds
sqrt (Sum rf) <= Sum (sqrt rf)