let A, B be 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:91;
then A4: rng (f | B) <> {} by RELAT_1:65;
consider x being Real such that
A5: x in B by SUBSET_1:10;
A6: (f | B) . x in rng (f | B) by A5, A3, FUNCT_1:def 5;
A7: rng f is bounded_below by A1, INTEGRA1:13;
hence A8: lower_bound (rng (f | B)) >= lower_bound (rng f) by A4, RELAT_1:99, SEQ_4:64; :: 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:99, XXREAL_2:44;
then A9: lower_bound (rng (f | B)) <= (f | B) . x by A6, SEQ_4:def 5;
A10: rng f is bounded_above by A1, INTEGRA1:15;
then rng (f | B) is bounded_above by RELAT_1:99, XXREAL_2:43;
then upper_bound (rng (f | B)) >= (f | B) . x by A6, SEQ_4:def 4;
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:99, SEQ_4:65; :: 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