theorem FS: :: NEWTON04:26

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