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

per cases ( r > 0 or r < 0 ) ;

suppose r > 0 ; :: thesis: ( f is without-infty & f is without+infty iff ( r (#) f is without-infty & r (#) f is without+infty ) )

hence ( f is without-infty & f is without+infty iff ( r (#) f is without-infty & r (#) f is without+infty ) ) by Th16, Th18; :: thesis: verum

end;

suppose r < 0 ; :: thesis: ( f is without-infty & f is without+infty iff ( r (#) f is without-infty & r (#) f is without+infty ) )

hence ( f is without-infty & f is without+infty iff ( r (#) f is without-infty & r (#) f is without+infty ) ) by Th17, Th19; :: thesis: verum

end;

end;