begin
Lm1:
for j being Element of NAT holds (j -' j) + 1 = 1
Lm2:
for n being Element of NAT st 1 <= n & n <= 2 & not n = 1 holds
n = 2
Lm3:
for A being non empty closed_interval Subset of REAL
for g being Function of A,REAL st g | A is bounded holds
upper_bound (rng g) >= lower_bound (rng g)
Lm4:
for A, B being non empty closed_interval Subset of REAL
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) )
Lm5:
for j being Element of NAT
for A being non empty closed_interval Subset of REAL
for D1 being Division of A st j in dom D1 holds
vol (divset (D1,j)) <= delta D1
Lm6:
for x being Real
for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for j1 being Element of NAT st j1 = (len D1) - 1 & x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} holds
rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)
Lm7:
for y being Real
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st vol A <> 0 & y in rng (lower_sum_set f) holds
ex D being Division of A st
( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A )
Lm8:
for A being non empty closed_interval Subset of REAL
for D1 being Division of A st vol A <> 0 & len D1 = 1 holds
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
Lm9:
for A being non empty closed_interval Subset of REAL
for D2 being Division of A st lower_bound A < D2 . 1 holds
<*(lower_bound A)*> ^ D2 is non empty increasing FinSequence of REAL
Lm10:
for A being non empty closed_interval Subset of REAL
for D1 being Division of A
for f being Function of A,REAL
for MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
( ( for i being Element of NAT st i in Seg (len D1) holds
divset (MD1,(i + 1)) = divset (D1,i) ) & upper_volume (f,D1) = (upper_volume (f,MD1)) /^ 1 & lower_volume (f,D1) = (lower_volume (f,MD1)) /^ 1 )
Lm11:
for A being non empty closed_interval Subset of REAL
for D2, MD2 being Division of A st MD2 = <*(lower_bound A)*> ^ D2 holds
vol (divset (MD2,1)) = 0
Lm12:
for A being non empty closed_interval Subset of REAL
for D1, MD1 being Division of A st MD1 = <*(lower_bound A)*> ^ D1 holds
delta MD1 = delta D1
theorem Th15:
for
r being
Real for
i,
j being
Element of
NAT for
A being non
empty closed_interval Subset of
REAL for
D1,
D2 being
Division of
A st
i in dom D1 &
j in dom D1 &
i <= j &
D1 <= D2 &
r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds
ex
B being non
empty closed_interval Subset of
REAL ex
MD1,
MD2 being
Division of
B st
(
r = lower_bound B &
upper_bound B = MD2 . (len MD2) &
upper_bound B = MD1 . (len MD1) &
MD1 <= MD2 &
MD1 = mid (
D1,
i,
j) &
MD2 = mid (
D2,
(indx (D2,D1,i)),
(indx (D2,D1,j))) )
begin