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