let f, g be nonnegative-yielding FinSequence of REAL ; :: thesis: (Sum f) * (Sum g) >= Sum (f (#) g)
A1: ( f (#) g is FinSequence of REAL & (Sum f) * g is FinSequence of REAL ) by NEWTON02:103;

now :: thesis: for i being Nat holds (f (#) g) . i <= ((Sum f) * g) . i

let i be Nat; :: thesis: (f (#) g) . i <= ((Sum f) * g) . i
(Sum f) * (g . i) = ((Sum f) (#) g) . i by VALUED_1:6;
hence (f (#) g) . i <= ((Sum f) * g) . i by FS; :: thesis: verum

end;

then Sum (f (#) g) <= Sum ((Sum f) * g) by A1, NYS;
hence (Sum f) * (Sum g) >= Sum (f (#) g) by RVSUM_1:87; :: thesis: verum