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:10;
then f . x <> +infty by XXREAL_3:def 5;
hence f . x < +infty by XXREAL_0:4; :: thesis: verum

end;

hence f is without+infty by MESFUNC5:11; :: thesis: verum