let Y, S be non empty set ; :: thesis: for F being Function of Y,S
for M being Function of S,ExtREAL st M is nonnegative holds
M * F is nonnegative
let F be Function of Y,S; :: thesis: for M being Function of S,ExtREAL st M is nonnegative holds
M * F is nonnegative
let M be Function of S,ExtREAL; :: thesis: ( M is nonnegative implies M * F is nonnegative )
assume A1: M is nonnegative ; :: thesis: M * F is nonnegative
for n being Element of Y holds 0. <= (M * F) . n

proof

let n be Element of Y; :: thesis: 0. <= (M * F) . n
dom (M * F) = Y by FUNCT_2:def 1;
then (M * F) . n = M . (F . n) by FUNCT_1:12;
hence 0. <= (M * F) . n by A1; :: thesis: verum

end;

hence M * F is nonnegative ; :: thesis: verum