let X be non empty set ; :: thesis: for r being negative Real
for f being Function of X,ExtREAL holds
( f is V121() iff r (#) f is V120() )
let r be negative Real; :: thesis: for f being Function of X,ExtREAL holds
( f is V121() iff r (#) f is V120() )
let f be Function of X,ExtREAL; :: thesis: ( f is V121() iff r (#) f is V120() )
thus ( f is V121() implies r (#) f is V120() ) ; :: thesis: ( r (#) f is V120() implies f is V121() )
assume A2: r (#) f is V120() ; :: thesis: f is V121()

now :: thesis: for x being set st x in dom f holds
f . x < +infty

let x be set ; :: thesis: ( x in dom f implies f . x < +infty )
assume x in dom f ; :: thesis: f . x < +infty
then A3: x in dom (r (#) f) by MESFUNC1:def 6;
then (r (#) f) . x = r * (f . x) by MESFUNC1:def 6;
then r * (f . x) > -infty by A2, A3, MESFUNC5:10;
then f . x <> +infty by XXREAL_3:def 5;
hence f . x < +infty by XXREAL_0:4; :: thesis: verum

end;

hence f is V121() by MESFUNC5:11; :: thesis: verum