let i be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for f being Function of A, REAL
for D being Element of divs A st f | A is bounded & i in dom D holds
upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f)
let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A, REAL
for D being Element of divs A st f | A is bounded & i in dom D holds
upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f)
let f be Function of A, REAL ; :: thesis: for D being Element of divs A st f | A is bounded & i in dom D holds
upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f)
let D be Element of divs A; :: thesis: ( f | A is bounded & i in dom D implies upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f) )
assume A1: f | A is bounded ; :: thesis: ( not i in dom D or upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f) )
assume i in dom D ; :: thesis: upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f)
then divset D,i c= A by INTEGRA1:10;
hence upper_bound (rng (f | (divset D,i))) >= lower_bound (rng f) by A1, Lm5; :: thesis: verum