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) . b1 > -infty )
assume A2: x in dom (r (#) f) ; :: thesis: (r (#) f) . b1 > -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) . b1 > -infty
then r * (f . x) > r * -infty by ;
then r * (f . x) > -infty by ;
hence (r (#) f) . x > -infty by ; :: thesis: verum
end;
suppose r = 0 ; :: thesis: (r (#) f) . b1 > -infty
then r * (f . x) > -infty ;
hence (r (#) f) . x > -infty by ; :: thesis: verum
end;
end;
end;
hence r (#) f is V120() by MESFUNC5:10; :: thesis: verum