let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being Function of A,REAL st f | A is bounded & i in dom D holds
lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f)
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for f being Function of A,REAL st f | A is bounded & i in dom D holds
lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f)
let D be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded & i in dom D holds
lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f)
let f be Function of A,REAL; :: thesis: ( f | A is bounded & i in dom D implies lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f) )
assume A1: f | A is bounded ; :: thesis: ( not i in dom D or lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f) )
assume i in dom D ; :: thesis: lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f)
then divset (D,i) c= A by INTEGRA1:8;
hence lower_bound (rng (f | (divset (D,i)))) <= upper_bound (rng f) by A1, Lm4; :: thesis: verum