let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds

for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded implies for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) )

assume A1: f | A is bounded ; :: thesis: for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) ; :: thesis: verum

for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded implies for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) )

assume A1: f | A is bounded ; :: thesis: for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

proof

hence
for D, D1 being Division of A ex D2 being Division of A st
let D, D1 be Division of A; :: thesis: ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

consider D2 being Division of A such that

A6: D <= D2 and

A7: D1 <= D2 and

A8: rng D2 = (rng D1) \/ (rng D) by Th4;

A9: (lower_sum (f,D2)) - (lower_sum (f,D1)) >= 0 by A1, A7, INTEGRA1:46, XREAL_1:48;

(lower_sum (f,D2)) - (lower_sum (f,D)) >= 0 by A1, A6, INTEGRA1:46, XREAL_1:48;

hence ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by A6, A7, A8, A9; :: thesis: verum

end;( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) )

consider D2 being Division of A such that

A6: D <= D2 and

A7: D1 <= D2 and

A8: rng D2 = (rng D1) \/ (rng D) by Th4;

A9: (lower_sum (f,D2)) - (lower_sum (f,D1)) >= 0 by A1, A7, INTEGRA1:46, XREAL_1:48;

(lower_sum (f,D2)) - (lower_sum (f,D)) >= 0 by A1, A6, INTEGRA1:46, XREAL_1:48;

hence ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by A6, A7, A8, A9; :: thesis: verum

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) ; :: thesis: verum