let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
rng (f | A) is real-bounded

let f be PartFunc of REAL,REAL; :: thesis: ( f | A is non-decreasing & A c= dom f implies rng (f | A) is real-bounded )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: rng (f | A) is real-bounded
A3: dom (f | A) = (dom f) /\ A by RELAT_1:61
.= A by ;
f . () is LowerBound of rng (f | A)
proof
lower_bound A <= upper_bound A by SEQ_4:11;
then lower_bound A in dom (f | A) by ;
then A4: lower_bound A in (dom f) /\ A by RELAT_1:61;
let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not y in rng (f | A) or f . () <= y )
assume y in rng (f | A) ; :: thesis: f . () <= y
then consider x being Element of REAL such that
A5: x in dom (f | A) and
A6: y = (f | A) . x by PARTFUN1:3;
A7: x in (dom f) /\ A by ;
( y = f . x & x >= lower_bound A ) by ;
hence f . () <= y by ; :: thesis: verum
end;
then A8: rng (f | A) is bounded_below ;
f . () is UpperBound of rng (f | A)
proof
lower_bound A <= upper_bound A by SEQ_4:11;
then upper_bound A in dom (f | A) by ;
then A9: upper_bound A in (dom f) /\ A by RELAT_1:61;
let y be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not y in rng (f | A) or y <= f . () )
assume y in rng (f | A) ; :: thesis: y <= f . ()
then consider x being Element of REAL such that
A10: x in dom (f | A) and
A11: y = (f | A) . x by PARTFUN1:3;
A12: x in (dom f) /\ A by ;
( y = f . x & x <= upper_bound A ) by ;
hence y <= f . () by ; :: thesis: verum
end;
then rng (f | A) is bounded_above ;
hence rng (f | A) is real-bounded by A8; :: thesis: verum