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

let f be PartFunc of REAL,REAL; :: thesis: ( f | A is non-decreasing & A c= dom f implies ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) )

assume that

A1: f | A is non-decreasing and

A2: A c= dom f ; :: thesis: ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )

A3: dom (f | A) = (dom f) /\ A by RELAT_1:61

.= A by A2, XBOOLE_1:28 ;

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 A3, INTEGRA2:1;

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

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

x >= a ) holds

f . (lower_bound A) >= a

for a being Real st ( for x being Real st x in rng (f | A) holds

x <= a ) holds

f . (upper_bound A) <= a

( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )

let f be PartFunc of REAL,REAL; :: thesis: ( f | A is non-decreasing & A c= dom f implies ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) )

assume that

A1: f | A is non-decreasing and

A2: A c= dom f ; :: thesis: ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )

A3: dom (f | A) = (dom f) /\ A by RELAT_1:61

.= A by A2, XBOOLE_1:28 ;

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 A3, INTEGRA2:1;

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

proof

A11:
lower_bound A in dom (f | A)
by A3, A5, INTEGRA2:1;
let y be Real; :: thesis: ( y in rng (f | A) implies 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

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 A9, INTEGRA2:1, RELAT_1:61;

then f . (upper_bound A) >= f . x by A1, A7, RFUNCT_2:24;

hence y <= f . (upper_bound A) by A9, A10, FUNCT_1:47; :: thesis: verum

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

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 A9, INTEGRA2:1, RELAT_1:61;

then f . (upper_bound A) >= f . x by A1, A7, RFUNCT_2:24;

hence y <= f . (upper_bound A) by A9, A10, FUNCT_1:47; :: thesis: verum

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

proof

for a being Real st ( for x being Real st x in rng (f | A) holds
let y be Real; :: thesis: ( y in rng (f | A) implies y >= f . (lower_bound A) )

assume y in rng (f | A) ; :: thesis: y >= f . (lower_bound A)

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 A14, INTEGRA2:1, RELAT_1:61;

then f . (lower_bound A) <= f . x by A1, A12, RFUNCT_2:24;

hence y >= f . (lower_bound A) by A14, A15, FUNCT_1:47; :: thesis: verum

end;assume y in rng (f | A) ; :: thesis: y >= f . (lower_bound A)

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 A14, INTEGRA2:1, RELAT_1:61;

then f . (lower_bound A) <= f . x by A1, A12, RFUNCT_2:24;

hence y >= f . (lower_bound A) by A14, A15, FUNCT_1:47; :: thesis: verum

x >= a ) holds

f . (lower_bound A) >= a

proof

hence
lower_bound (rng (f | A)) = f . (lower_bound A)
by A4, A13, SEQ_4:44; :: thesis: upper_bound (rng (f | A)) = f . (upper_bound A)
let a be Real; :: thesis: ( ( for x being Real st x in rng (f | A) holds

x >= a ) implies f . (lower_bound A) >= a )

assume A16: for x being Real st x in rng (f | A) holds

x >= a ; :: thesis: f . (lower_bound A) >= a

( f . (lower_bound A) = (f | A) . (lower_bound A) & (f | A) . (lower_bound A) in rng (f | A) ) by A11, FUNCT_1:47, FUNCT_1:def 3;

hence f . (lower_bound A) >= a by A16; :: thesis: verum

end;x >= a ) implies f . (lower_bound A) >= a )

assume A16: for x being Real st x in rng (f | A) holds

x >= a ; :: thesis: f . (lower_bound A) >= a

( f . (lower_bound A) = (f | A) . (lower_bound A) & (f | A) . (lower_bound A) in rng (f | A) ) by A11, FUNCT_1:47, FUNCT_1:def 3;

hence f . (lower_bound A) >= a by A16; :: thesis: verum

for a being Real st ( for x being Real st x in rng (f | A) holds

x <= a ) holds

f . (upper_bound A) <= a

proof

hence
upper_bound (rng (f | A)) = f . (upper_bound A)
by A4, A8, SEQ_4:46; :: thesis: verum
let a be Real; :: thesis: ( ( for x being Real st x in rng (f | A) holds

x <= a ) implies f . (upper_bound A) <= a )

assume A17: for x being Real st x in rng (f | A) holds

x <= a ; :: thesis: f . (upper_bound A) <= a

( f . (upper_bound A) = (f | A) . (upper_bound A) & (f | A) . (upper_bound A) in rng (f | A) ) by A6, FUNCT_1:47, FUNCT_1:def 3;

hence f . (upper_bound A) <= a by A17; :: thesis: verum

end;x <= a ) implies f . (upper_bound A) <= a )

assume A17: for x being Real st x in rng (f | A) holds

x <= a ; :: thesis: f . (upper_bound A) <= a

( f . (upper_bound A) = (f | A) . (upper_bound A) & (f | A) . (upper_bound A) in rng (f | A) ) by A6, FUNCT_1:47, FUNCT_1:def 3;

hence f . (upper_bound A) <= a by A17; :: thesis: verum