let A, B be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded & B c= A holds

( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded & B c= A implies ( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) ) )

assume that

A1: f | A is bounded and

A2: B c= A ; :: thesis: ( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

B c= dom f by A2, FUNCT_2:def 1;

then A3: dom (f | B) = B by RELAT_1:62;

then A4: rng (f | B) <> {} by RELAT_1:42;

consider x being Element of REAL such that

A5: x in B by SUBSET_1:4;

A6: (f | B) . x in rng (f | B) by A5, A3, FUNCT_1:def 3;

A7: rng f is bounded_below by A1, INTEGRA1:11;

hence A8: lower_bound (rng (f | B)) >= lower_bound (rng f) by A4, RELAT_1:70, SEQ_4:47; :: thesis: ( lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

rng (f | B) is bounded_below by A7, RELAT_1:70, XXREAL_2:44;

then A9: lower_bound (rng (f | B)) <= (f | B) . x by A6, SEQ_4:def 2;

A10: rng f is bounded_above by A1, INTEGRA1:13;

then rng (f | B) is bounded_above by RELAT_1:70, XXREAL_2:43;

then upper_bound (rng (f | B)) >= (f | B) . x by A6, SEQ_4:def 1;

then A11: lower_bound (rng (f | B)) <= upper_bound (rng (f | B)) by A9, XXREAL_0:2;

hence upper_bound (rng (f | B)) >= lower_bound (rng f) by A8, XXREAL_0:2; :: thesis: ( upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

thus upper_bound (rng (f | B)) <= upper_bound (rng f) by A10, A4, RELAT_1:70, SEQ_4:48; :: thesis: lower_bound (rng (f | B)) <= upper_bound (rng f)

hence lower_bound (rng (f | B)) <= upper_bound (rng f) by A11, XXREAL_0:2; :: thesis: verum

( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded & B c= A implies ( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) ) )

assume that

A1: f | A is bounded and

A2: B c= A ; :: thesis: ( lower_bound (rng (f | B)) >= lower_bound (rng f) & lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

B c= dom f by A2, FUNCT_2:def 1;

then A3: dom (f | B) = B by RELAT_1:62;

then A4: rng (f | B) <> {} by RELAT_1:42;

consider x being Element of REAL such that

A5: x in B by SUBSET_1:4;

A6: (f | B) . x in rng (f | B) by A5, A3, FUNCT_1:def 3;

A7: rng f is bounded_below by A1, INTEGRA1:11;

hence A8: lower_bound (rng (f | B)) >= lower_bound (rng f) by A4, RELAT_1:70, SEQ_4:47; :: thesis: ( lower_bound (rng f) <= upper_bound (rng (f | B)) & upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

rng (f | B) is bounded_below by A7, RELAT_1:70, XXREAL_2:44;

then A9: lower_bound (rng (f | B)) <= (f | B) . x by A6, SEQ_4:def 2;

A10: rng f is bounded_above by A1, INTEGRA1:13;

then rng (f | B) is bounded_above by RELAT_1:70, XXREAL_2:43;

then upper_bound (rng (f | B)) >= (f | B) . x by A6, SEQ_4:def 1;

then A11: lower_bound (rng (f | B)) <= upper_bound (rng (f | B)) by A9, XXREAL_0:2;

hence upper_bound (rng (f | B)) >= lower_bound (rng f) by A8, XXREAL_0:2; :: thesis: ( upper_bound (rng (f | B)) <= upper_bound (rng f) & lower_bound (rng (f | B)) <= upper_bound (rng f) )

thus upper_bound (rng (f | B)) <= upper_bound (rng f) by A10, A4, RELAT_1:70, SEQ_4:48; :: thesis: lower_bound (rng (f | B)) <= upper_bound (rng f)

hence lower_bound (rng (f | B)) <= upper_bound (rng f) by A11, XXREAL_0:2; :: thesis: verum