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

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 without-infty by MESFUNC5:10; :: thesis: verum