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()
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 V121() by MESFUNC5:11; :: thesis: verum