let X be non empty set ; :: thesis: for r being Real

for f being V121() Function of X,ExtREAL st r >= 0 holds

r (#) f is V121()

let r be Real; :: thesis: for f being V121() Function of X,ExtREAL st r >= 0 holds

r (#) f is V121()

let f be V121() Function of X,ExtREAL; :: thesis: ( r >= 0 implies r (#) f is V121() )

assume A1: r >= 0 ; :: thesis: r (#) f is V121()

for f being V121() Function of X,ExtREAL st r >= 0 holds

r (#) f is V121()

let r be Real; :: thesis: for f being V121() Function of X,ExtREAL st r >= 0 holds

r (#) f is V121()

let f be V121() Function of X,ExtREAL; :: thesis: ( r >= 0 implies r (#) f is V121() )

assume A1: r >= 0 ; :: thesis: r (#) f is V121()

now :: thesis: for x being set st x in dom (r (#) f) holds

(r (#) f) . x < +infty

hence
r (#) f is V121()
by MESFUNC5:11; :: thesis: verum(r (#) f) . x < +infty

let x be set ; :: thesis: ( x in dom (r (#) f) implies (r (#) f) . b_{1} < +infty )

assume A2: x in dom (r (#) f) ; :: thesis: (r (#) f) . b_{1} < +infty

then A3: x in dom f by MESFUNC1:def 6;

end;assume A2: x in dom (r (#) f) ; :: thesis: (r (#) f) . b

then A3: x in dom f by MESFUNC1:def 6;