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
( inf (rng (f | A)) = f . (inf A) & sup (rng (f | A)) = f . (sup A) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | A is non-decreasing & A c= dom f implies ( inf (rng (f | A)) = f . (inf A) & sup (rng (f | A)) = f . (sup A) ) )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: ( inf (rng (f | A)) = f . (inf A) & sup (rng (f | A)) = f . (sup A) )
A3: dom (f | A) = (dom f) /\ A by RELAT_1:90
.= A by A2, XBOOLE_1:28 ;
then A4: rng (f | A) <> {} by RELAT_1:65;
inf A <= sup A by SEQ_4:24;
then A5: ( sup A in dom (f | A) & inf A in dom (f | A) ) by A3, INTEGRA2:1;
then A6: ( sup A in (dom f) /\ A & inf A in (dom f) /\ A ) by RELAT_1:90;
A7: 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: x in (dom f) /\ A by A8, RELAT_1:90;
inf A <= x by A3, A8, INTEGRA2:1;
then f . (inf A) <= f . x by A1, A6, A9, RFUNCT_2:48;
hence y >= f . (inf A) by A8, FUNCT_1:70; :: thesis: verum

end;

for a being real number st ( for x being real number st x in rng (f | A) holds
x >= a ) holds
f . (inf A) >= a

proof

let a be real number ; :: thesis: ( ( for x being real number st x in rng (f | A) holds
x >= a ) implies f . (inf A) >= a )
assume A10: for x being real number st x in rng (f | A) holds
x >= a ; :: thesis: f . (inf A) >= a
A11: f . (inf A) = (f | A) . (inf A) by A5, FUNCT_1:70;
(f | A) . (inf A) in rng (f | A) by A5, FUNCT_1:def 5;
hence f . (inf A) >= a by A10, A11; :: thesis: verum

end;

hence inf (rng (f | A)) = f . (inf A) by A4, A7, SEQ_4:61; :: thesis: sup (rng (f | A)) = f . (sup A)
A12: for x being real number st x in rng (f | A) holds
x <= 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
A13: ( x in dom (f | A) & y = (f | A) . x ) by PARTFUN1:26;
A14: x in (dom f) /\ A by A13, RELAT_1:90;
sup A >= x by A3, A13, INTEGRA2:1;
then f . (sup A) >= f . x by A1, A6, A14, RFUNCT_2:48;
hence y <= f . (sup A) by A13, FUNCT_1:70; :: thesis: verum

end;

for a being real number st ( for x being real number st x in rng (f | A) holds
x <= a ) holds
f . (sup A) <= a

proof

let a be real number ; :: thesis: ( ( for x being real number st x in rng (f | A) holds
x <= a ) implies f . (sup A) <= a )
assume A15: for x being real number st x in rng (f | A) holds
x <= a ; :: thesis: f . (sup A) <= a
A16: f . (sup A) = (f | A) . (sup A) by A5, FUNCT_1:70;
(f | A) . (sup A) in rng (f | A) by A5, FUNCT_1:def 5;
hence f . (sup A) <= a by A15, A16; :: thesis: verum

end;

hence sup (rng (f | A)) = f . (sup A) by A4, A12, SEQ_4:63; :: thesis: verum