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

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