for f, g being nonnegative-yielding FinSequence of REAL holds (Sum f) * (Sum g) >= Sum (f (#) g)