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;
A5: inf A <= sup A by SEQ_4:24;
then A6: sup A in dom (f | A) by A3, INTEGRA2:1;
then A7: sup A in (dom f) /\ A by RELAT_1:90;
A8: 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
A9: x in dom (f | A) and
A10: y = (f | A) . x by PARTFUN1:26;
( x in (dom f) /\ A & sup A >= x ) by A3, A9, INTEGRA2:1, RELAT_1:90;
then f . (sup A) >= f . x by A1, A7, RFUNCT_2:48;
hence y <= f . (sup A) by A9, A10, FUNCT_1:70; :: thesis: verum

end;

A11: inf A in dom (f | A) by A3, A5, INTEGRA2:1;
then A12: inf A in (dom f) /\ A by RELAT_1:90;
A13: 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
A14: x in dom (f | A) and
A15: y = (f | A) . x by PARTFUN1:26;
( x in (dom f) /\ A & inf A <= x ) by A3, A14, INTEGRA2:1, RELAT_1:90;
then f . (inf A) <= f . x by A1, A12, RFUNCT_2:48;
hence y >= f . (inf A) by A14, A15, 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 A16: for x being real number st x in rng (f | A) holds
x >= a ; :: thesis: f . (inf A) >= a
( f . (inf A) = (f | A) . (inf A) & (f | A) . (inf A) in rng (f | A) ) by A11, FUNCT_1:70, FUNCT_1:def 5;
hence f . (inf A) >= a by A16; :: thesis: verum

end;

hence inf (rng (f | A)) = f . (inf A) by A4, A13, SEQ_4:61; :: thesis: sup (rng (f | A)) = f . (sup A)
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 A17: for x being real number st x in rng (f | A) holds
x <= a ; :: thesis: f . (sup A) <= a
( f . (sup A) = (f | A) . (sup A) & (f | A) . (sup A) in rng (f | A) ) by A6, FUNCT_1:70, FUNCT_1:def 5;
hence f . (sup A) <= a by A17; :: thesis: verum

end;

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