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 A1: ( f | A is bounded & 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) )
then ( f | A is bounded_above & f | A is bounded_below ) ;
then A2: ( rng f is bounded_above & rng f is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
consider x being Real such that
A3: x in B by SUBSET_1:10;
B c= dom f by A1, FUNCT_2:def 1;
then A4: dom (f | B) = B by RELAT_1:91;
then A5: (f | B) . x in rng (f | B) by A3, FUNCT_1:def 5;
A6: rng (f | B) <> {} by A4, RELAT_1:65;
rng (f | B) c= rng f by RELAT_1:99;
then A7: ( rng (f | B) is bounded_above & rng (f | B) is bounded_below ) by A2, XXREAL_2:43, XXREAL_2:44;
thus A8: lower_bound (rng (f | B)) >= lower_bound (rng f) by A2, A6, 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) )
A9: lower_bound (rng (f | B)) <= (f | B) . x by A5, A7, SEQ_4:def 5;
upper_bound (rng (f | B)) >= (f | B) . x by A5, A7, SEQ_4:def 4;
then A10: 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 A2, A6, 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 A10, XXREAL_0:2; :: thesis: verum