let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st rng f is real-bounded holds
f is V71()
let f be PartFunc of X,ExtREAL; :: thesis: ( rng f is real-bounded implies f is V71() )
assume A1: rng f is real-bounded ; :: thesis: f is V71()
then rng f is bounded_above by XXREAL_2:def 11;
then consider UB being Real such that
A2: UB is UpperBound of rng f by XXREAL_2:def 10;
A3: UB in REAL by XREAL_0:def 1;
rng f is bounded_below by A1, XXREAL_2:def 11;
then consider LB being Real such that
A4: LB is LowerBound of rng f by XXREAL_2:def 9;
A5: LB in REAL by XREAL_0:def 1;
now :: thesis: for x being Element of X st x in dom f holds
|.(f . x).| < +infty
let x be Element of X; :: thesis: ( x in dom f implies |.(f . x).| < +infty )
assume x in dom f ; :: thesis: |.(f . x).| < +infty
then A6: f . x in rng f by FUNCT_1:3;
then LB <= f . x by A4, XXREAL_2:def 2;
then -infty < f . x by A5, XXREAL_0:2, XXREAL_0:12;
then A7: - +infty < f . x by XXREAL_3:23;
f . x <= UB by A2, A6, XXREAL_2:def 1;
then f . x < +infty by A3, XXREAL_0:2, XXREAL_0:9;
hence |.(f . x).| < +infty by A7, EXTREAL1:22; :: thesis: verum
end;
hence f is V71() by MESFUNC2:def 1; :: thesis: verum