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