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
( lower_bound (rng (f | A)) = f . () & upper_bound (rng (f | A)) = f . () )

let f be PartFunc of REAL,REAL; :: thesis: ( f | A is non-decreasing & A c= dom f implies ( lower_bound (rng (f | A)) = f . () & upper_bound (rng (f | A)) = f . () ) )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; :: thesis: ( lower_bound (rng (f | A)) = f . () & upper_bound (rng (f | A)) = f . () )
A3: dom (f | A) = (dom f) /\ A by RELAT_1:61
.= A by ;
then A4: rng (f | A) <> {} by RELAT_1:42;
A5: lower_bound A <= upper_bound A by SEQ_4:11;
then A6: upper_bound A in dom (f | A) by ;
then A7: upper_bound A in (dom f) /\ A by RELAT_1:61;
A8: for x being Real st x in rng (f | A) holds
x <= f . ()
proof
let y be Real; :: thesis: ( y in rng (f | A) implies y <= f . () )
assume y in rng (f | A) ; :: thesis: y <= f . ()
then consider x being Element of REAL such that
A9: x in dom (f | A) and
A10: y = (f | A) . x by PARTFUN1:3;
( x in (dom f) /\ A & upper_bound A >= x ) by ;
then f . () >= f . x by ;
hence y <= f . () by ; :: thesis: verum
end;
A11: lower_bound A in dom (f | A) by ;
then A12: lower_bound A in (dom f) /\ A by RELAT_1:61;
A13: for y being Real st y in rng (f | A) holds
y >= f . ()
proof
let y be Real; :: thesis: ( y in rng (f | A) implies y >= f . () )
assume y in rng (f | A) ; :: thesis: y >= f . ()
then consider x being Element of REAL such that
A14: x in dom (f | A) and
A15: y = (f | A) . x by PARTFUN1:3;
( x in (dom f) /\ A & lower_bound A <= x ) by ;
then f . () <= f . x by ;
hence y >= f . () by ; :: thesis: verum
end;
for a being Real st ( for x being Real st x in rng (f | A) holds
x >= a ) holds
f . () >= a
proof
let a be Real; :: thesis: ( ( for x being Real st x in rng (f | A) holds
x >= a ) implies f . () >= a )

assume A16: for x being Real st x in rng (f | A) holds
x >= a ; :: thesis: f . () >= a
( f . () = (f | A) . () & (f | A) . () in rng (f | A) ) by ;
hence f . () >= a by A16; :: thesis: verum
end;
hence lower_bound (rng (f | A)) = f . () by ; :: thesis: upper_bound (rng (f | A)) = f . ()
for a being Real st ( for x being Real st x in rng (f | A) holds
x <= a ) holds
f . () <= a
proof
let a be Real; :: thesis: ( ( for x being Real st x in rng (f | A) holds
x <= a ) implies f . () <= a )

assume A17: for x being Real st x in rng (f | A) holds
x <= a ; :: thesis: f . () <= a
( f . () = (f | A) . () & (f | A) . () in rng (f | A) ) by ;
hence f . () <= a by A17; :: thesis: verum
end;
hence upper_bound (rng (f | A)) = f . () by ; :: thesis: verum