let Y, S be non empty set ; :: thesis: for F being PartFunc of Y,S
for M being Function of S,ExtREAL st M is nonnegative holds
M * F is nonnegative
let F be PartFunc 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

now :: thesis: for n being object holds (M * F) . n >= 0

let n be object ; :: thesis: (M * F) . b₁ >= 0

per cases ( n in dom (M * F) or not n in dom (M * F) ) ;

suppose n in dom (M * F) ; :: thesis: (M * F) . b₁ >= 0

then (M * F) . n = M . (F . n) by FUNCT_1:12;
hence (M * F) . n >= 0 by A1, SUPINF_2:51; :: thesis: verum

end;

suppose not n in dom (M * F) ; :: thesis: (M * F) . b₁ >= 0

hence (M * F) . n >= 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence M * F is nonnegative by SUPINF_2:51; :: thesis: verum