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

per cases ( n in dom (f (#) g) or not n in dom (f (#) g) ) ;

suppose n in dom (f (#) g) ; :: thesis: (f (#) g) . n <= (Sum f) * (g . n)

then (f (#) g) . n = (f . n) * (g . n) by VALUED_1:def 4;
hence (f (#) g) . n <= (Sum f) * (g . n) by SN, XREAL_1:64; :: thesis: verum

end;

suppose not n in dom (f (#) g) ; :: thesis: (f (#) g) . n <= (Sum f) * (g . n)

hence (f (#) g) . n <= (Sum f) * (g . n) by FUNCT_1:def 2; :: thesis: verum

end;

end;