let X be non empty set ; :: thesis:
let r be Real; :: thesis:
let f be V121() Function of X,ExtREAL; :: thesis:
assume A1: r <= 0 ; :: thesis:

let x be set ; :: thesis:
assume A2: x in dom (r (#) f) ; :: thesis:
then A3: x in dom f by MESFUNC1:def 6;

per cases by A1;

suppose A4: r < 0 ; :: thesis:

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

end;

suppose r = 0 ; :: thesis:

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

end;

end;

end;

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