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 V94() holds
M * F is V94()
let F be Function of Y,S; :: thesis: for M being Function of S,ExtREAL st M is V94() holds
M * F is V94()
let M be Function of S,ExtREAL; :: thesis: ( M is V94() implies M * F is V94() )
assume A1: M is V94() ; :: thesis: M * F is V94()
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 V94() ; :: thesis: verum