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 A2, XBOOLE_1:28 ;

f . (lower_bound A) is LowerBound of rng (f | A)

f . (upper_bound A) is UpperBound of rng (f | A)

hence rng (f | A) is real-bounded by A8; :: thesis: verum

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 A2, XBOOLE_1:28 ;

f . (lower_bound A) is LowerBound of rng (f | A)

proof

then A8:
rng (f | A) is bounded_below
;
lower_bound A <= upper_bound A
by SEQ_4:11;

then lower_bound A in dom (f | A) by A3, INTEGRA2:1;

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 . (lower_bound A) <= y )

assume y in rng (f | A) ; :: thesis: f . (lower_bound A) <= 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 A5, RELAT_1:61;

( y = f . x & x >= lower_bound A ) by A5, A6, FUNCT_1:47, INTEGRA2:1;

hence f . (lower_bound A) <= y by A1, A7, A4, RFUNCT_2:24; :: thesis: verum

end;then lower_bound A in dom (f | A) by A3, INTEGRA2:1;

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 . (lower_bound A) <= y )

assume y in rng (f | A) ; :: thesis: f . (lower_bound A) <= 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 A5, RELAT_1:61;

( y = f . x & x >= lower_bound A ) by A5, A6, FUNCT_1:47, INTEGRA2:1;

hence f . (lower_bound A) <= y by A1, A7, A4, RFUNCT_2:24; :: thesis: verum

f . (upper_bound A) is UpperBound of rng (f | A)

proof

then
rng (f | A) is bounded_above
;
lower_bound A <= upper_bound A
by SEQ_4:11;

then upper_bound A in dom (f | A) by A3, INTEGRA2:1;

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 . (upper_bound A) )

assume y in rng (f | A) ; :: thesis: y <= f . (upper_bound A)

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 A10, RELAT_1:61;

( y = f . x & x <= upper_bound A ) by A10, A11, FUNCT_1:47, INTEGRA2:1;

hence y <= f . (upper_bound A) by A1, A12, A9, RFUNCT_2:24; :: thesis: verum

end;then upper_bound A in dom (f | A) by A3, INTEGRA2:1;

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 . (upper_bound A) )

assume y in rng (f | A) ; :: thesis: y <= f . (upper_bound A)

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 A10, RELAT_1:61;

( y = f . x & x <= upper_bound A ) by A10, A11, FUNCT_1:47, INTEGRA2:1;

hence y <= f . (upper_bound A) by A1, A12, A9, RFUNCT_2:24; :: thesis: verum

hence rng (f | A) is real-bounded by A8; :: thesis: verum