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