let A be 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 bounded
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | A is non-decreasing & A c= dom f implies rng (f | A) is bounded )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: rng (f | A) is bounded
A3: dom (f | A) = (dom f) /\ A by RELAT_1:90
.= A by A2, XBOOLE_1:28 ;
for y being real number st y in rng (f | A) holds
y <= f . (sup A)

proof

let y be real number ; :: thesis: ( y in rng (f | A) implies y <= f . (sup A) )
assume y in rng (f | A) ; :: thesis: y <= f . (sup A)
then consider x being Real such that
A4: ( x in dom (f | A) & y = (f | A) . x ) by PARTFUN1:26;
A5: y = f . x by A4, FUNCT_1:70;
A6: x <= sup A by A3, A4, INTEGRA2:1;
inf A <= sup A by SEQ_4:24;
then sup A in dom (f | A) by A3, INTEGRA2:1;
then ( x in (dom f) /\ A & sup A in (dom f) /\ A ) by A4, RELAT_1:90;
hence y <= f . (sup A) by A1, A5, A6, RFUNCT_2:48; :: thesis: verum

end;

then A7: rng (f | A) is bounded_above by SEQ_4:def 1;
for y being real number st y in rng (f | A) holds
y >= f . (inf A)

proof

let y be real number ; :: thesis: ( y in rng (f | A) implies y >= f . (inf A) )
assume y in rng (f | A) ; :: thesis: y >= f . (inf A)
then consider x being Real such that
A8: ( x in dom (f | A) & y = (f | A) . x ) by PARTFUN1:26;
A9: y = f . x by A8, FUNCT_1:70;
A10: x >= inf A by A3, A8, INTEGRA2:1;
inf A <= sup A by SEQ_4:24;
then inf A in dom (f | A) by A3, INTEGRA2:1;
then ( x in (dom f) /\ A & inf A in (dom f) /\ A ) by A8, RELAT_1:90;
hence y >= f . (inf A) by A1, A9, A10, RFUNCT_2:48; :: thesis: verum

end;

then rng (f | A) is bounded_below by SEQ_4:def 2;
hence rng (f | A) is bounded by A7; :: thesis: verum