let X be non empty set ; :: thesis: for r being negative Real
for f being Function of X,ExtREAL holds
( f is V120() iff r (#) f is V121() )
let r be negative Real; :: thesis: for f being Function of X,ExtREAL holds
( f is V120() iff r (#) f is V121() )
let f be Function of X,ExtREAL; :: thesis: ( f is V120() iff r (#) f is V121() )
thus ( f is V120() implies r (#) f is V121() ) ; :: thesis: ( r (#) f is V121() implies f is V120() )
assume A2: r (#) f is V121() ; :: thesis: f is V120()
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:11;
then f . x <> -infty by XXREAL_3:def 5;
hence f . x > -infty by XXREAL_0:6; :: thesis: verum
end;
hence f is V120() by MESFUNC5:10; :: thesis: verum