theorem :: NEWTON04:40

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