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 V224() holds
M * F is nonnegative
let F be PartFunc of Y,S; :: thesis: for M being Function of S,ExtREAL st M is V224() holds
M * F is nonnegative
let M be Function of S,ExtREAL; :: thesis: ( M is V224() implies M * F is nonnegative )
assume A1: M is V224() ; :: thesis: M * F is nonnegative
now :: thesis: for n being object holds (M * F) . n >= 0
let n be object ; :: thesis: (M * F) . b1 >= 0
per cases ( n in dom (M * F) or not n in dom (M * F) ) ;
suppose n in dom (M * F) ; :: thesis: (M * F) . b1 >= 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) . b1 >= 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