let f, g be real-valued nonnegative-yielding FinSequence; :: thesis: (Sum f) * (Sum g) >= Sum (f (#) g)

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 NYS;
hence (Sum f) * (Sum g) >= Sum (f (#) g) by RVSUM_1:87; :: thesis: verum