let X be non empty set ; :: thesis: for r being Real
for f being V120() Function of X,ExtREAL st r >= 0 holds
r (#) f is V120()
let r be Real; :: thesis: for f being V120() Function of X,ExtREAL st r >= 0 holds
r (#) f is V120()
let f be V120() Function of X,ExtREAL; :: thesis: ( r >= 0 implies r (#) f is V120() )
assume A1: r >= 0 ; :: thesis: r (#) f is V120()

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

let x be set ; :: thesis: ( x in dom (r (#) f) implies (r (#) f) . b₁ > -infty )
assume A2: x in dom (r (#) f) ; :: thesis: (r (#) f) . b₁ > -infty
then A3: x in dom f by MESFUNC1:def 6;

per cases ( r > 0 or r = 0 ) by A1;

suppose A4: r > 0 ; :: thesis: (r (#) f) . b₁ > -infty

then r * (f . x) > r * -infty by A3, MESFUNC5:10, XXREAL_3:72;
then r * (f . x) > -infty by A4, XXREAL_3:def 5;
hence (r (#) f) . x > -infty by A2, MESFUNC1:def 6; :: thesis: verum

end;

suppose r = 0 ; :: thesis: (r (#) f) . b₁ > -infty

then r * (f . x) > -infty ;
hence (r (#) f) . x > -infty by A2, MESFUNC1:def 6; :: thesis: verum

end;

end;

end;

hence r (#) f is V120() by MESFUNC5:10; :: thesis: verum