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

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

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

hence ( r (#) f is without-infty & r (#) f is without+infty ) ; :: thesis: verum

end;

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

hence ( r (#) f is without-infty & r (#) f is without+infty ) ; :: thesis: verum

end;

end;