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

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

hence
M * F is V94()
; :: thesis: verum
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;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