let X, Y be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for r being Real st f = Y --> r holds
( f is without-infty & f is without+infty )
let f be PartFunc of X,ExtREAL; :: thesis: for r being Real st f = Y --> r holds
( f is without-infty & f is without+infty )
let r be Real; :: thesis: ( f = Y --> r implies ( f is without-infty & f is without+infty ) )
assume A1: f = Y --> r ; :: thesis: ( f is without-infty & f is without+infty )
then for x being object holds f . x > -infty by XREAL_0:def 1, XXREAL_0:12;
hence f is without-infty by MESFUNC5:def 5; :: thesis: f is without+infty
for x being object holds f . x < +infty by A1, XREAL_0:def 1, XXREAL_0:9;
hence f is without+infty by MESFUNC5:def 6; :: thesis: verum