for n being Nat
for f, g being nonnegative-yielding FinSequence of REAL holds (f (#) g) . n <= (Sum f) * (g . n)