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

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