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()

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

hence
f is V121()
by MESFUNC5:11; :: thesis: verumf . 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;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