let x be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

let D1, D2 be Division of A; :: thesis: for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

let g be Function of A,REAL; :: thesis: ( x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded implies (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

assume that

A1: x in divset (D1,(len D1)) and

A2: len D1 >= 2 ; :: thesis: ( not D1 <= D2 or not rng D2 = (rng D1) \/ {x} or not g | A is bounded or (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

set j = len D1;

assume that

A3: D1 <= D2 and

A4: rng D2 = (rng D1) \/ {x} ; :: thesis: ( not g | A is bounded or (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

A5: len D1 in dom D1 by FINSEQ_5:6;

then A6: indx (D2,D1,(len D1)) in dom D2 by A3, INTEGRA1:def 19;

A7: len D1 <> 1 by A2;

then reconsider j1 = (len D1) - 1 as Element of NAT by A5, INTEGRA1:7;

A8: j1 in dom D1 by A5, A7, INTEGRA1:7;

then A9: j1 <= len D1 by FINSEQ_3:25;

A10: 1 <= j1 by A8, FINSEQ_3:25;

then mid (D1,1,j1) is increasing by A5, A7, INTEGRA1:7, INTEGRA1:35;

then A11: D1 | j1 is increasing by A10, FINSEQ_6:116;

A12: (len D1) - 1 in dom D1 by A5, A7, INTEGRA1:7;

then A13: indx (D2,D1,j1) in dom D2 by A3, INTEGRA1:def 19;

then A14: 1 <= indx (D2,D1,j1) by FINSEQ_3:25;

then mid (D2,1,(indx (D2,D1,j1))) is increasing by A13, INTEGRA1:35;

then A15: D2 | (indx (D2,D1,j1)) is increasing by A14, FINSEQ_6:116;

A16: indx (D2,D1,j1) <= len D2 by A13, FINSEQ_3:25;

then A17: len (D2 | (indx (D2,D1,j1))) = indx (D2,D1,j1) by FINSEQ_1:59;

A18: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A1, A2, A3, A4, Lm6;

then A19: D2 | (indx (D2,D1,j1)) = D1 | j1 by A15, A11, Th6;

A20: for k being Element of NAT st 1 <= k & k <= j1 holds

k = indx (D2,D1,k)

((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k

deffunc H_{1}( Division of A) -> FinSequence of REAL = lower_volume (g,$1);

deffunc H_{2}( Division of A, Nat) -> set = (PartSums (lower_volume (g,$1))) . $2;

A67: len D1 >= len (lower_volume (g,D1)) by INTEGRA1:def 7;

A68: len D1 <= len H_{1}(D1)
by INTEGRA1:def 7;

A69: len D1 in Seg (len D1) by FINSEQ_1:3;

then A70: 1 <= len D1 by FINSEQ_1:1;

then A71: len D1 in dom H_{1}(D1)
by A68, FINSEQ_3:25;

assume A72: g | A is bounded ; :: thesis: (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

len D1 < (len D1) + 1 by NAT_1:13;

then A73: j1 < len D1 by XREAL_1:19;

then j1 < len H_{1}(D1)
by INTEGRA1:def 7;

then j1 in dom H_{1}(D1)
by A10, FINSEQ_3:25;

then H_{2}(D1,j1) = Sum (H_{1}(D1) | j1)
by INTEGRA1:def 20;

then H_{2}(D1,j1) + (Sum (mid (H_{1}(D1),(len D1),(len D1)))) =
Sum ((H_{1}(D1) | j1) ^ (mid (H_{1}(D1),(len D1),(len D1))))
by RVSUM_1:75

.= Sum ((mid (H_{1}(D1),1,j1)) ^ (mid (H_{1}(D1),(j1 + 1),(len D1))))
by A10, FINSEQ_6:116

.= Sum (mid (H_{1}(D1),1,(len D1)))
by A10, A68, A73, INTEGRA2:4

.= Sum (H_{1}(D1) | (len D1))
by A70, FINSEQ_6:116
;

then A74: H_{2}(D1,j1) + (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) = H_{2}(D1, len D1)
by A71, INTEGRA1:def 20;

A75: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then A76: indx (D2,D1,(len D1)) in Seg (len D2) by FINSEQ_1:def 3;

then A77: 1 <= indx (D2,D1,(len D1)) by FINSEQ_1:1;

len D1 < (len D1) + 1 by NAT_1:13;

then j1 < len D1 by XREAL_1:19;

then A78: indx (D2,D1,j1) < indx (D2,D1,(len D1)) by A3, A5, A8, Th8;

then A79: (indx (D2,D1,j1)) + 1 <= indx (D2,D1,(len D1)) by NAT_1:13;

A80: j1 in dom D1 by A5, A7, INTEGRA1:7;

A81: (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

then indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;

then A153: indx (D2,D1,j1) <= len (lower_volume (g,D2)) by INTEGRA1:def 7;

j1 <= len D1 by A12, FINSEQ_3:25;

then A154: j1 <= len (lower_volume (g,D1)) by INTEGRA1:def 7;

A155: D2 . (indx (D2,D1,(len D1))) = D1 . (len D1) by A3, A5, INTEGRA1:def 19;

A156: indx (D2,D1,(len D1)) >= len (lower_volume (g,D2))

then indx (D2,D1,(len D1)) in Seg (len (lower_volume (g,D2))) by INTEGRA1:def 7;

then indx (D2,D1,(len D1)) in dom (lower_volume (g,D2)) by FINSEQ_1:def 3;

then A159: H_{2}(D2, indx (D2,D1,(len D1))) =
Sum ((lower_volume (g,D2)) | (indx (D2,D1,(len D1))))
by INTEGRA1:def 20

.= Sum (lower_volume (g,D2)) by A156, FINSEQ_1:58 ;

len D1 in Seg (len (lower_volume (g,D1))) by A69, INTEGRA1:def 7;

then len D1 in dom (lower_volume (g,D1)) by FINSEQ_1:def 3;

then A160: H_{2}(D1, len D1) =
Sum ((lower_volume (g,D1)) | (len D1))
by INTEGRA1:def 20

.= Sum (lower_volume (g,D1)) by A67, FINSEQ_1:58 ;

len D1 = len (lower_volume (g,D1)) by INTEGRA1:def 7;

then A161: j1 in dom (lower_volume (g,D1)) by A8, FINSEQ_3:29;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A15, A11, A18, Th6;

then indx (D2,D1,j1) = j1 by A9, A17, FINSEQ_1:59;

then len ((lower_volume (g,D1)) | j1) = indx (D2,D1,j1) by A154, FINSEQ_1:59;

then len ((lower_volume (g,D1)) | j1) = len ((lower_volume (g,D2)) | (indx (D2,D1,j1))) by A153, FINSEQ_1:59;

then A162: (lower_volume (g,D2)) | (indx (D2,D1,j1)) = (lower_volume (g,D1)) | j1 by A38, FINSEQ_1:14;

len D2 = len (lower_volume (g,D2)) by INTEGRA1:def 7;

then indx (D2,D1,j1) in dom (lower_volume (g,D2)) by A13, FINSEQ_3:29;

then A163: H_{2}(D2, indx (D2,D1,j1)) =
Sum ((lower_volume (g,D2)) | (indx (D2,D1,j1)))
by INTEGRA1:def 20

.= H_{2}(D1,j1)
by A162, A161, INTEGRA1:def 20
;

indx (D2,D1,(len D1)) <= len D2 by A76, FINSEQ_1:1;

then A164: indx (D2,D1,(len D1)) <= len H_{1}(D2)
by INTEGRA1:def 7;

A165: len D2 = len H_{1}(D2)
by INTEGRA1:def 7;

then A166: indx (D2,D1,(len D1)) in dom H_{1}(D2)
by A75, FINSEQ_3:29;

indx (D2,D1,j1) in dom H_{1}(D2)
by A13, A165, FINSEQ_3:29;

then H_{2}(D2, indx (D2,D1,j1)) = Sum (H_{1}(D2) | (indx (D2,D1,j1)))
by INTEGRA1:def 20;

then H_{2}(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) =
Sum ((H_{1}(D2) | (indx (D2,D1,j1))) ^ (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))))
by RVSUM_1:75

.= Sum ((mid (H_{1}(D2),1,(indx (D2,D1,j1)))) ^ (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))))
by A14, FINSEQ_6:116

.= Sum (mid (H_{1}(D2),1,(indx (D2,D1,(len D1)))))
by A14, A78, A164, INTEGRA2:4

.= Sum (H_{1}(D2) | (indx (D2,D1,(len D1))))
by A77, FINSEQ_6:116
;

then H_{2}(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) = H_{2}(D2, indx (D2,D1,(len D1)))
by A166, INTEGRA1:def 20;

hence (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A163, A81, A74, A159, A160; :: thesis: verum

for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A

for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

let D1, D2 be Division of A; :: thesis: for g being Function of A,REAL st x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded holds

(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

let g be Function of A,REAL; :: thesis: ( x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded implies (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

assume that

A1: x in divset (D1,(len D1)) and

A2: len D1 >= 2 ; :: thesis: ( not D1 <= D2 or not rng D2 = (rng D1) \/ {x} or not g | A is bounded or (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

set j = len D1;

assume that

A3: D1 <= D2 and

A4: rng D2 = (rng D1) \/ {x} ; :: thesis: ( not g | A is bounded or (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

A5: len D1 in dom D1 by FINSEQ_5:6;

then A6: indx (D2,D1,(len D1)) in dom D2 by A3, INTEGRA1:def 19;

A7: len D1 <> 1 by A2;

then reconsider j1 = (len D1) - 1 as Element of NAT by A5, INTEGRA1:7;

A8: j1 in dom D1 by A5, A7, INTEGRA1:7;

then A9: j1 <= len D1 by FINSEQ_3:25;

A10: 1 <= j1 by A8, FINSEQ_3:25;

then mid (D1,1,j1) is increasing by A5, A7, INTEGRA1:7, INTEGRA1:35;

then A11: D1 | j1 is increasing by A10, FINSEQ_6:116;

A12: (len D1) - 1 in dom D1 by A5, A7, INTEGRA1:7;

then A13: indx (D2,D1,j1) in dom D2 by A3, INTEGRA1:def 19;

then A14: 1 <= indx (D2,D1,j1) by FINSEQ_3:25;

then mid (D2,1,(indx (D2,D1,j1))) is increasing by A13, INTEGRA1:35;

then A15: D2 | (indx (D2,D1,j1)) is increasing by A14, FINSEQ_6:116;

A16: indx (D2,D1,j1) <= len D2 by A13, FINSEQ_3:25;

then A17: len (D2 | (indx (D2,D1,j1))) = indx (D2,D1,j1) by FINSEQ_1:59;

A18: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A1, A2, A3, A4, Lm6;

then A19: D2 | (indx (D2,D1,j1)) = D1 | j1 by A15, A11, Th6;

A20: for k being Element of NAT st 1 <= k & k <= j1 holds

k = indx (D2,D1,k)

proof

A38:
for k being Nat st 1 <= k & k <= len ((lower_volume (g,D1)) | j1) holds
let k be Element of NAT ; :: thesis: ( 1 <= k & k <= j1 implies k = indx (D2,D1,k) )

assume that

A21: 1 <= k and

A22: k <= j1 ; :: thesis: k = indx (D2,D1,k)

assume A23: k <> indx (D2,D1,k) ; :: thesis: contradiction

end;assume that

A21: 1 <= k and

A22: k <= j1 ; :: thesis: k = indx (D2,D1,k)

assume A23: k <> indx (D2,D1,k) ; :: thesis: contradiction

per cases
( k > indx (D2,D1,k) or k < indx (D2,D1,k) )
by A23, XXREAL_0:1;

end;

suppose A24:
k > indx (D2,D1,k)
; :: thesis: contradiction

k <= len D1
by A9, A22, XXREAL_0:2;

then A25: k in dom D1 by A21, FINSEQ_3:25;

then indx (D2,D1,k) in dom D2 by A3, INTEGRA1:def 19;

then indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;

then A26: 1 <= indx (D2,D1,k) by FINSEQ_1:1;

A27: indx (D2,D1,k) < j1 by A22, A24, XXREAL_0:2;

then A28: indx (D2,D1,k) in Seg j1 by A26, FINSEQ_1:1;

indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A8, A22, A25, Th7;

then indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A26, FINSEQ_1:1;

then A29: (D2 | (indx (D2,D1,j1))) . (indx (D2,D1,k)) = D2 . (indx (D2,D1,k)) by A13, RFINSEQ:6;

indx (D2,D1,k) <= len D1 by A9, A27, XXREAL_0:2;

then indx (D2,D1,k) in dom D1 by A26, FINSEQ_3:25;

then A30: D1 . k > D1 . (indx (D2,D1,k)) by A24, A25, SEQM_3:def 1;

D1 . k = D2 . (indx (D2,D1,k)) by A3, A25, INTEGRA1:def 19;

hence contradiction by A8, A19, A29, A30, A28, RFINSEQ:6; :: thesis: verum

end;then A25: k in dom D1 by A21, FINSEQ_3:25;

then indx (D2,D1,k) in dom D2 by A3, INTEGRA1:def 19;

then indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;

then A26: 1 <= indx (D2,D1,k) by FINSEQ_1:1;

A27: indx (D2,D1,k) < j1 by A22, A24, XXREAL_0:2;

then A28: indx (D2,D1,k) in Seg j1 by A26, FINSEQ_1:1;

indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A8, A22, A25, Th7;

then indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A26, FINSEQ_1:1;

then A29: (D2 | (indx (D2,D1,j1))) . (indx (D2,D1,k)) = D2 . (indx (D2,D1,k)) by A13, RFINSEQ:6;

indx (D2,D1,k) <= len D1 by A9, A27, XXREAL_0:2;

then indx (D2,D1,k) in dom D1 by A26, FINSEQ_3:25;

then A30: D1 . k > D1 . (indx (D2,D1,k)) by A24, A25, SEQM_3:def 1;

D1 . k = D2 . (indx (D2,D1,k)) by A3, A25, INTEGRA1:def 19;

hence contradiction by A8, A19, A29, A30, A28, RFINSEQ:6; :: thesis: verum

suppose A31:
k < indx (D2,D1,k)
; :: thesis: contradiction

k <= len D1
by A9, A22, XXREAL_0:2;

then A32: k in dom D1 by A21, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A8, A22, Th7;

then A33: k <= indx (D2,D1,j1) by A31, XXREAL_0:2;

then k <= len D2 by A16, XXREAL_0:2;

then A34: k in dom D2 by A21, FINSEQ_3:25;

k in Seg j1 by A21, A22, FINSEQ_1:1;

then A35: D1 . k = (D1 | j1) . k by A12, RFINSEQ:6;

indx (D2,D1,k) in dom D2 by A3, A32, INTEGRA1:def 19;

then A36: D2 . k < D2 . (indx (D2,D1,k)) by A31, A34, SEQM_3:def 1;

A37: k in Seg (indx (D2,D1,j1)) by A21, A33, FINSEQ_1:1;

D1 . k = D2 . (indx (D2,D1,k)) by A3, A32, INTEGRA1:def 19;

hence contradiction by A13, A19, A35, A36, A37, RFINSEQ:6; :: thesis: verum

end;then A32: k in dom D1 by A21, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A8, A22, Th7;

then A33: k <= indx (D2,D1,j1) by A31, XXREAL_0:2;

then k <= len D2 by A16, XXREAL_0:2;

then A34: k in dom D2 by A21, FINSEQ_3:25;

k in Seg j1 by A21, A22, FINSEQ_1:1;

then A35: D1 . k = (D1 | j1) . k by A12, RFINSEQ:6;

indx (D2,D1,k) in dom D2 by A3, A32, INTEGRA1:def 19;

then A36: D2 . k < D2 . (indx (D2,D1,k)) by A31, A34, SEQM_3:def 1;

A37: k in Seg (indx (D2,D1,j1)) by A21, A33, FINSEQ_1:1;

D1 . k = D2 . (indx (D2,D1,k)) by A3, A32, INTEGRA1:def 19;

hence contradiction by A13, A19, A35, A36, A37, RFINSEQ:6; :: thesis: verum

((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k

proof

A66:
len D2 in dom D2
by FINSEQ_5:6;
indx (D2,D1,j1) in Seg (len D2)
by A13, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len (lower_volume (g,D2))) by INTEGRA1:def 7;

then A39: indx (D2,D1,j1) in dom (lower_volume (g,D2)) by FINSEQ_1:def 3;

let k be Nat; :: thesis: ( 1 <= k & k <= len ((lower_volume (g,D1)) | j1) implies ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k )

assume that

A40: 1 <= k and

A41: k <= len ((lower_volume (g,D1)) | j1) ; :: thesis: ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A42: len (lower_volume (g,D1)) = len D1 by INTEGRA1:def 7;

then A43: k <= j1 by A9, A41, FINSEQ_1:59;

then k <= len D1 by A9, XXREAL_0:2;

then k in Seg (len D1) by A40, FINSEQ_1:1;

then A44: k in dom D1 by FINSEQ_1:def 3;

then A45: indx (D2,D1,k) in dom D2 by A3, INTEGRA1:def 19;

A46: k in Seg j1 by A40, A43, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A20, A40, A43;

then A47: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A10, A20;

then indx (D2,D1,k) <= indx (D2,D1,j1) by FINSEQ_1:1;

then A48: indx (D2,D1,k) <= len D2 by A16, XXREAL_0:2;

A49: D1 . k = D2 . (indx (D2,D1,k)) by A3, A44, INTEGRA1:def 19;

A50: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

then A63: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A50, INTEGRA1:4;

j1 in Seg (len (lower_volume (g,D1))) by A8, A42, FINSEQ_1:def 3;

then j1 in dom (lower_volume (g,D1)) by FINSEQ_1:def 3;

then A64: ((lower_volume (g,D1)) | j1) . k = (lower_volume (g,D1)) . k by A46, RFINSEQ:6

.= (lower_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A44, A63, INTEGRA1:def 7 ;

1 <= indx (D2,D1,k) by A20, A40, A43;

then A65: indx (D2,D1,k) in dom D2 by A48, FINSEQ_3:25;

((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A20, A40, A43

.= (lower_volume (g,D2)) . (indx (D2,D1,k)) by A47, A39, RFINSEQ:6

.= (lower_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A65, INTEGRA1:def 7 ;

hence ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k by A64; :: thesis: verum

end;then indx (D2,D1,j1) in Seg (len (lower_volume (g,D2))) by INTEGRA1:def 7;

then A39: indx (D2,D1,j1) in dom (lower_volume (g,D2)) by FINSEQ_1:def 3;

let k be Nat; :: thesis: ( 1 <= k & k <= len ((lower_volume (g,D1)) | j1) implies ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k )

assume that

A40: 1 <= k and

A41: k <= len ((lower_volume (g,D1)) | j1) ; :: thesis: ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A42: len (lower_volume (g,D1)) = len D1 by INTEGRA1:def 7;

then A43: k <= j1 by A9, A41, FINSEQ_1:59;

then k <= len D1 by A9, XXREAL_0:2;

then k in Seg (len D1) by A40, FINSEQ_1:1;

then A44: k in dom D1 by FINSEQ_1:def 3;

then A45: indx (D2,D1,k) in dom D2 by A3, INTEGRA1:def 19;

A46: k in Seg j1 by A40, A43, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A20, A40, A43;

then A47: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A10, A20;

then indx (D2,D1,k) <= indx (D2,D1,j1) by FINSEQ_1:1;

then A48: indx (D2,D1,k) <= len D2 by A16, XXREAL_0:2;

A49: D1 . k = D2 . (indx (D2,D1,k)) by A3, A44, INTEGRA1:def 19;

A50: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

proof
end;

divset (D1,k) = [.(lower_bound (divset (D1,k))),(upper_bound (divset (D1,k))).]
by INTEGRA1:4;per cases
( k = 1 or k <> 1 )
;

end;

suppose A51:
k = 1
; :: thesis: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

then A52:
upper_bound (divset (D1,k)) = D1 . k
by A44, INTEGRA1:def 4;

A53: lower_bound (divset (D1,k)) = lower_bound A by A44, A51, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A10, A20, A51;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A45, A49, A53, A52, INTEGRA1:def 4; :: thesis: verum

end;A53: lower_bound (divset (D1,k)) = lower_bound A by A44, A51, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A10, A20, A51;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A45, A49, A53, A52, INTEGRA1:def 4; :: thesis: verum

suppose A54:
k <> 1
; :: thesis: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

then reconsider k1 = k - 1 as Element of NAT by A44, INTEGRA1:7;

A55: k - 1 in dom D1 by A44, A54, INTEGRA1:7;

then A56: 1 <= k1 by FINSEQ_3:25;

k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A57: k1 <= j1 by A43, XXREAL_0:2;

A58: indx (D2,D1,k) <> 1 by A20, A40, A43, A54;

then A59: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A45, INTEGRA1:def 4;

A60: upper_bound (divset (D1,k)) = D1 . k by A44, A54, INTEGRA1:def 4;

A61: lower_bound (divset (D1,k)) = D1 . (k - 1) by A44, A54, INTEGRA1:def 4;

A62: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A45, A58, INTEGRA1:def 4;

D2 . ((indx (D2,D1,k)) - 1) = D2 . (k - 1) by A20, A40, A43

.= D2 . (indx (D2,D1,k1)) by A20, A57, A56 ;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A3, A44, A61, A60, A55, A59, A62, INTEGRA1:def 19; :: thesis: verum

end;A55: k - 1 in dom D1 by A44, A54, INTEGRA1:7;

then A56: 1 <= k1 by FINSEQ_3:25;

k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A57: k1 <= j1 by A43, XXREAL_0:2;

A58: indx (D2,D1,k) <> 1 by A20, A40, A43, A54;

then A59: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A45, INTEGRA1:def 4;

A60: upper_bound (divset (D1,k)) = D1 . k by A44, A54, INTEGRA1:def 4;

A61: lower_bound (divset (D1,k)) = D1 . (k - 1) by A44, A54, INTEGRA1:def 4;

A62: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A45, A58, INTEGRA1:def 4;

D2 . ((indx (D2,D1,k)) - 1) = D2 . (k - 1) by A20, A40, A43

.= D2 . (indx (D2,D1,k1)) by A20, A57, A56 ;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A3, A44, A61, A60, A55, A59, A62, INTEGRA1:def 19; :: thesis: verum

then A63: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A50, INTEGRA1:4;

j1 in Seg (len (lower_volume (g,D1))) by A8, A42, FINSEQ_1:def 3;

then j1 in dom (lower_volume (g,D1)) by FINSEQ_1:def 3;

then A64: ((lower_volume (g,D1)) | j1) . k = (lower_volume (g,D1)) . k by A46, RFINSEQ:6

.= (lower_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A44, A63, INTEGRA1:def 7 ;

1 <= indx (D2,D1,k) by A20, A40, A43;

then A65: indx (D2,D1,k) in dom D2 by A48, FINSEQ_3:25;

((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A20, A40, A43

.= (lower_volume (g,D2)) . (indx (D2,D1,k)) by A47, A39, RFINSEQ:6

.= (lower_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A65, INTEGRA1:def 7 ;

hence ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k by A64; :: thesis: verum

deffunc H

deffunc H

A67: len D1 >= len (lower_volume (g,D1)) by INTEGRA1:def 7;

A68: len D1 <= len H

A69: len D1 in Seg (len D1) by FINSEQ_1:3;

then A70: 1 <= len D1 by FINSEQ_1:1;

then A71: len D1 in dom H

assume A72: g | A is bounded ; :: thesis: (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

len D1 < (len D1) + 1 by NAT_1:13;

then A73: j1 < len D1 by XREAL_1:19;

then j1 < len H

then j1 in dom H

then H

then H

.= Sum ((mid (H

.= Sum (mid (H

.= Sum (H

then A74: H

A75: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then A76: indx (D2,D1,(len D1)) in Seg (len D2) by FINSEQ_1:def 3;

then A77: 1 <= indx (D2,D1,(len D1)) by FINSEQ_1:1;

len D1 < (len D1) + 1 by NAT_1:13;

then j1 < len D1 by XREAL_1:19;

then A78: indx (D2,D1,j1) < indx (D2,D1,(len D1)) by A3, A5, A8, Th8;

then A79: (indx (D2,D1,j1)) + 1 <= indx (D2,D1,(len D1)) by NAT_1:13;

A80: j1 in dom D1 by A5, A7, INTEGRA1:7;

A81: (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

proof

indx (D2,D1,j1) in dom D2
by A3, A12, INTEGRA1:def 19;
A82:
(indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) <= 2

A106: 1 <= len D1 by A69, FINSEQ_1:1;

then A107: (mid ((lower_volume (g,D1)),(len D1),(len D1))) . 1 = (lower_volume (g,D1)) . (len D1) by A105, FINSEQ_6:118;

reconsider lv = (lower_volume (g,D1)) . (len D1) as Element of REAL by XREAL_0:def 1;

((len D1) -' (len D1)) + 1 = 1 by Lm1;

then len (mid ((lower_volume (g,D1)),(len D1),(len D1))) = 1 by A106, A105, FINSEQ_6:118;

then A108: mid ((lower_volume (g,D1)),(len D1),(len D1)) = <*lv*> by A107, FINSEQ_1:40;

A109: 1 <= (indx (D2,D1,j1)) + 1 by A14, NAT_1:13;

indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then A110: indx (D2,D1,(len D1)) in Seg (len D2) by FINSEQ_1:def 3;

then A111: 1 <= indx (D2,D1,(len D1)) by FINSEQ_1:1;

indx (D2,D1,(len D1)) in Seg (len (lower_volume (g,D2))) by A110, INTEGRA1:def 7;

then A112: indx (D2,D1,(len D1)) <= len (lower_volume (g,D2)) by FINSEQ_1:1;

then A113: (indx (D2,D1,j1)) + 1 <= len (lower_volume (g,D2)) by A79, XXREAL_0:2;

then (indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (g,D2))) by A109, FINSEQ_1:1;

then A114: (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

(indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1) = (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) by A79, XREAL_1:233;

then ((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 <= 2 by A82;

then A115: len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= 2 by A79, A111, A112, A109, A113, FINSEQ_6:118;

len (lower_volume (g,D2)) = len D2 by INTEGRA1:def 7;

then A116: (indx (D2,D1,j1)) + 1 in dom D2 by A109, A113, FINSEQ_3:25;

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 >= 0 + 1 by XREAL_1:6;

then A117: 1 <= len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) by A79, A111, A112, A109, A113, FINSEQ_6:118;

end;proof

A105:
len D1 <= len (lower_volume (g,D1))
by INTEGRA1:def 7;
set ID1 = (indx (D2,D1,j1)) + 1;

set ID2 = ((indx (D2,D1,j1)) + 1) + 1;

assume (indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) > 2 ; :: thesis: contradiction

then A83: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,(len D1)) by XREAL_1:20;

A84: (indx (D2,D1,j1)) + 1 < ((indx (D2,D1,j1)) + 1) + 1 by NAT_1:13;

then indx (D2,D1,j1) <= ((indx (D2,D1,j1)) + 1) + 1 by NAT_1:13;

then A85: 1 <= ((indx (D2,D1,j1)) + 1) + 1 by A14, XXREAL_0:2;

A86: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then A87: indx (D2,D1,(len D1)) <= len D2 by FINSEQ_3:25;

then ((indx (D2,D1,j1)) + 1) + 1 <= len D2 by A83, XXREAL_0:2;

then A88: ((indx (D2,D1,j1)) + 1) + 1 in dom D2 by A85, FINSEQ_3:25;

then A89: D2 . (((indx (D2,D1,j1)) + 1) + 1) < D2 . (indx (D2,D1,(len D1))) by A83, A86, SEQM_3:def 1;

A90: 1 <= (indx (D2,D1,j1)) + 1 by A14, NAT_1:13;

A91: D1 . j1 = D2 . (indx (D2,D1,j1)) by A3, A8, INTEGRA1:def 19;

(indx (D2,D1,j1)) + 1 <= indx (D2,D1,(len D1)) by A83, A84, XXREAL_0:2;

then (indx (D2,D1,j1)) + 1 <= len D2 by A87, XXREAL_0:2;

then A92: (indx (D2,D1,j1)) + 1 in dom D2 by A90, FINSEQ_3:25;

A93: D1 . (len D1) = D2 . (indx (D2,D1,(len D1))) by A3, A5, INTEGRA1:def 19;

indx (D2,D1,j1) < (indx (D2,D1,j1)) + 1 by NAT_1:13;

then A94: D2 . (indx (D2,D1,j1)) < D2 . ((indx (D2,D1,j1)) + 1) by A13, A92, SEQM_3:def 1;

A95: D2 . ((indx (D2,D1,j1)) + 1) < D2 . (((indx (D2,D1,j1)) + 1) + 1) by A84, A92, A88, SEQM_3:def 1;

A96: ( not D2 . ((indx (D2,D1,j1)) + 1) in rng D1 & not D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )

then D2 . ((indx (D2,D1,j1)) + 1) in {x} by A4, A96, XBOOLE_0:def 3;

then A104: D2 . ((indx (D2,D1,j1)) + 1) = x by TARSKI:def 1;

D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D2 by A88, FUNCT_1:def 3;

then D2 . (((indx (D2,D1,j1)) + 1) + 1) in {x} by A4, A96, XBOOLE_0:def 3;

then D2 . ((indx (D2,D1,j1)) + 1) = D2 . (((indx (D2,D1,j1)) + 1) + 1) by A104, TARSKI:def 1;

hence contradiction by A84, A92, A88, SEQ_4:138; :: thesis: verum

end;set ID2 = ((indx (D2,D1,j1)) + 1) + 1;

assume (indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) > 2 ; :: thesis: contradiction

then A83: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,(len D1)) by XREAL_1:20;

A84: (indx (D2,D1,j1)) + 1 < ((indx (D2,D1,j1)) + 1) + 1 by NAT_1:13;

then indx (D2,D1,j1) <= ((indx (D2,D1,j1)) + 1) + 1 by NAT_1:13;

then A85: 1 <= ((indx (D2,D1,j1)) + 1) + 1 by A14, XXREAL_0:2;

A86: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then A87: indx (D2,D1,(len D1)) <= len D2 by FINSEQ_3:25;

then ((indx (D2,D1,j1)) + 1) + 1 <= len D2 by A83, XXREAL_0:2;

then A88: ((indx (D2,D1,j1)) + 1) + 1 in dom D2 by A85, FINSEQ_3:25;

then A89: D2 . (((indx (D2,D1,j1)) + 1) + 1) < D2 . (indx (D2,D1,(len D1))) by A83, A86, SEQM_3:def 1;

A90: 1 <= (indx (D2,D1,j1)) + 1 by A14, NAT_1:13;

A91: D1 . j1 = D2 . (indx (D2,D1,j1)) by A3, A8, INTEGRA1:def 19;

(indx (D2,D1,j1)) + 1 <= indx (D2,D1,(len D1)) by A83, A84, XXREAL_0:2;

then (indx (D2,D1,j1)) + 1 <= len D2 by A87, XXREAL_0:2;

then A92: (indx (D2,D1,j1)) + 1 in dom D2 by A90, FINSEQ_3:25;

A93: D1 . (len D1) = D2 . (indx (D2,D1,(len D1))) by A3, A5, INTEGRA1:def 19;

indx (D2,D1,j1) < (indx (D2,D1,j1)) + 1 by NAT_1:13;

then A94: D2 . (indx (D2,D1,j1)) < D2 . ((indx (D2,D1,j1)) + 1) by A13, A92, SEQM_3:def 1;

A95: D2 . ((indx (D2,D1,j1)) + 1) < D2 . (((indx (D2,D1,j1)) + 1) + 1) by A84, A92, A88, SEQM_3:def 1;

A96: ( not D2 . ((indx (D2,D1,j1)) + 1) in rng D1 & not D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )

proof

D2 . ((indx (D2,D1,j1)) + 1) in rng D2
by A92, FUNCT_1:def 3;
assume A97:
( D2 . ((indx (D2,D1,j1)) + 1) in rng D1 or D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )
; :: thesis: contradiction

end;per cases
( D2 . ((indx (D2,D1,j1)) + 1) in rng D1 or D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )
by A97;

end;

suppose
D2 . ((indx (D2,D1,j1)) + 1) in rng D1
; :: thesis: contradiction

then consider n being Element of NAT such that

A98: n in dom D1 and

A99: D1 . n = D2 . ((indx (D2,D1,j1)) + 1) by PARTFUN1:3;

j1 < n by A80, A94, A91, A98, A99, SEQ_4:137;

then A100: len D1 < n + 1 by XREAL_1:19;

D2 . ((indx (D2,D1,j1)) + 1) < D2 . (indx (D2,D1,(len D1))) by A95, A89, XXREAL_0:2;

then n < len D1 by A5, A93, A98, A99, SEQ_4:137;

hence contradiction by A100, NAT_1:13; :: thesis: verum

end;A98: n in dom D1 and

A99: D1 . n = D2 . ((indx (D2,D1,j1)) + 1) by PARTFUN1:3;

j1 < n by A80, A94, A91, A98, A99, SEQ_4:137;

then A100: len D1 < n + 1 by XREAL_1:19;

D2 . ((indx (D2,D1,j1)) + 1) < D2 . (indx (D2,D1,(len D1))) by A95, A89, XXREAL_0:2;

then n < len D1 by A5, A93, A98, A99, SEQ_4:137;

hence contradiction by A100, NAT_1:13; :: thesis: verum

suppose
D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1
; :: thesis: contradiction

then consider n being Element of NAT such that

A101: n in dom D1 and

A102: D1 . n = D2 . (((indx (D2,D1,j1)) + 1) + 1) by PARTFUN1:3;

D2 . (indx (D2,D1,j1)) < D2 . (((indx (D2,D1,j1)) + 1) + 1) by A94, A95, XXREAL_0:2;

then j1 < n by A8, A91, A101, A102, SEQ_4:137;

then A103: len D1 < n + 1 by XREAL_1:19;

n < len D1 by A5, A89, A93, A101, A102, SEQ_4:137;

hence contradiction by A103, NAT_1:13; :: thesis: verum

end;A101: n in dom D1 and

A102: D1 . n = D2 . (((indx (D2,D1,j1)) + 1) + 1) by PARTFUN1:3;

D2 . (indx (D2,D1,j1)) < D2 . (((indx (D2,D1,j1)) + 1) + 1) by A94, A95, XXREAL_0:2;

then j1 < n by A8, A91, A101, A102, SEQ_4:137;

then A103: len D1 < n + 1 by XREAL_1:19;

n < len D1 by A5, A89, A93, A101, A102, SEQ_4:137;

hence contradiction by A103, NAT_1:13; :: thesis: verum

then D2 . ((indx (D2,D1,j1)) + 1) in {x} by A4, A96, XBOOLE_0:def 3;

then A104: D2 . ((indx (D2,D1,j1)) + 1) = x by TARSKI:def 1;

D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D2 by A88, FUNCT_1:def 3;

then D2 . (((indx (D2,D1,j1)) + 1) + 1) in {x} by A4, A96, XBOOLE_0:def 3;

then D2 . ((indx (D2,D1,j1)) + 1) = D2 . (((indx (D2,D1,j1)) + 1) + 1) by A104, TARSKI:def 1;

hence contradiction by A84, A92, A88, SEQ_4:138; :: thesis: verum

A106: 1 <= len D1 by A69, FINSEQ_1:1;

then A107: (mid ((lower_volume (g,D1)),(len D1),(len D1))) . 1 = (lower_volume (g,D1)) . (len D1) by A105, FINSEQ_6:118;

reconsider lv = (lower_volume (g,D1)) . (len D1) as Element of REAL by XREAL_0:def 1;

((len D1) -' (len D1)) + 1 = 1 by Lm1;

then len (mid ((lower_volume (g,D1)),(len D1),(len D1))) = 1 by A106, A105, FINSEQ_6:118;

then A108: mid ((lower_volume (g,D1)),(len D1),(len D1)) = <*lv*> by A107, FINSEQ_1:40;

A109: 1 <= (indx (D2,D1,j1)) + 1 by A14, NAT_1:13;

indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then A110: indx (D2,D1,(len D1)) in Seg (len D2) by FINSEQ_1:def 3;

then A111: 1 <= indx (D2,D1,(len D1)) by FINSEQ_1:1;

indx (D2,D1,(len D1)) in Seg (len (lower_volume (g,D2))) by A110, INTEGRA1:def 7;

then A112: indx (D2,D1,(len D1)) <= len (lower_volume (g,D2)) by FINSEQ_1:1;

then A113: (indx (D2,D1,j1)) + 1 <= len (lower_volume (g,D2)) by A79, XXREAL_0:2;

then (indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (g,D2))) by A109, FINSEQ_1:1;

then A114: (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

(indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1) = (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) by A79, XREAL_1:233;

then ((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 <= 2 by A82;

then A115: len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= 2 by A79, A111, A112, A109, A113, FINSEQ_6:118;

len (lower_volume (g,D2)) = len D2 by INTEGRA1:def 7;

then A116: (indx (D2,D1,j1)) + 1 in dom D2 by A109, A113, FINSEQ_3:25;

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 >= 0 + 1 by XREAL_1:6;

then A117: 1 <= len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) by A79, A111, A112, A109, A113, FINSEQ_6:118;

now :: thesis: (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)end;

hence
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
; :: thesis: verumper cases
( len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 1 or len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 2 )
by A117, A115, Lm2;

end;

suppose A118:
len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 1
; :: thesis: (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

upper_bound (divset (D1,(len D1))) = D1 . (len D1)
by A5, A7, INTEGRA1:def 4;

then A119: upper_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,(len D1))) by A3, A5, INTEGRA1:def 19;

lower_bound (divset (D1,(len D1))) = D1 . j1 by A5, A7, INTEGRA1:def 4;

then lower_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,j1)) by A3, A8, INTEGRA1:def 19;

then A120: divset (D1,(len D1)) = [.(D2 . (indx (D2,D1,j1))),(D2 . (indx (D2,D1,(len D1)))).] by A119, INTEGRA1:4;

A121: delta D1 >= 0 by Th9;

A122: (upper_bound (rng g)) - (lower_bound (rng g)) >= 0 by A72, Lm3, XREAL_1:48;

A123: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = ((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 by A79, A111, A112, A109, A113, FINSEQ_6:118;

then A124: (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) = 0 by A79, A118, XREAL_1:233;

then indx (D2,D1,(len D1)) <> 1 by A13, FINSEQ_3:25;

then A125: upper_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . (indx (D2,D1,(len D1))) by A123, INTEGRA1:def 4;

lower_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . ((indx (D2,D1,(len D1))) - 1) by A14, A124, A123, INTEGRA1:def 4;

then A126: divset (D2,(indx (D2,D1,(len D1)))) = divset (D1,(len D1)) by A124, A120, A125, INTEGRA1:4;

reconsider li = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) as Element of REAL by XREAL_0:def 1;

(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1 = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) by A111, A112, A109, A113, FINSEQ_6:118;

then mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))) = <*li*> by A118, FINSEQ_1:40;

then Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) by FINSOP_1:11

.= (lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A116, INTEGRA1:def 7

.= (lower_volume (g,D1)) . (len D1) by A5, A124, A126, INTEGRA1:def 7

.= Sum (mid ((lower_volume (g,D1)),(len D1),(len D1))) by A108, FINSOP_1:11 ;

hence (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A121, A122; :: thesis: verum

end;then A119: upper_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,(len D1))) by A3, A5, INTEGRA1:def 19;

lower_bound (divset (D1,(len D1))) = D1 . j1 by A5, A7, INTEGRA1:def 4;

then lower_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,j1)) by A3, A8, INTEGRA1:def 19;

then A120: divset (D1,(len D1)) = [.(D2 . (indx (D2,D1,j1))),(D2 . (indx (D2,D1,(len D1)))).] by A119, INTEGRA1:4;

A121: delta D1 >= 0 by Th9;

A122: (upper_bound (rng g)) - (lower_bound (rng g)) >= 0 by A72, Lm3, XREAL_1:48;

A123: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = ((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 by A79, A111, A112, A109, A113, FINSEQ_6:118;

then A124: (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) = 0 by A79, A118, XREAL_1:233;

then indx (D2,D1,(len D1)) <> 1 by A13, FINSEQ_3:25;

then A125: upper_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . (indx (D2,D1,(len D1))) by A123, INTEGRA1:def 4;

lower_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . ((indx (D2,D1,(len D1))) - 1) by A14, A124, A123, INTEGRA1:def 4;

then A126: divset (D2,(indx (D2,D1,(len D1)))) = divset (D1,(len D1)) by A124, A120, A125, INTEGRA1:4;

reconsider li = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) as Element of REAL by XREAL_0:def 1;

(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1 = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) by A111, A112, A109, A113, FINSEQ_6:118;

then mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))) = <*li*> by A118, FINSEQ_1:40;

then Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) by FINSOP_1:11

.= (lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A116, INTEGRA1:def 7

.= (lower_volume (g,D1)) . (len D1) by A5, A124, A126, INTEGRA1:def 7

.= Sum (mid ((lower_volume (g,D1)),(len D1),(len D1))) by A108, FINSOP_1:11 ;

hence (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A121, A122; :: thesis: verum

suppose A127:
len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 2
; :: thesis: (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)

A128:
(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1 = (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)
by A111, A112, A109, A113, FINSEQ_6:118;

A129: 2 + ((indx (D2,D1,j1)) + 1) >= 0 + 1 by XREAL_1:7;

(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 2 = H_{1}(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1)
by A79, A111, A112, A109, A113, A127, FINSEQ_6:118

.= H_{1}(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) - 1)
by A129, XREAL_1:233

.= H_{1}(D2) . ((indx (D2,D1,j1)) + (1 + 1))
;

then mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))) = <*((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)),((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 2))*> by A127, A128, FINSEQ_1:44;

then A130: Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = ((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)) + ((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 2)) by RVSUM_1:77;

A131: vol (divset (D2,((indx (D2,D1,j1)) + 1))) >= 0 by INTEGRA1:9;

upper_bound (divset (D1,(len D1))) = D1 . (len D1) by A5, A7, INTEGRA1:def 4;

then A132: upper_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,(len D1))) by A3, A5, INTEGRA1:def 19;

A133: vol (divset (D2,((indx (D2,D1,j1)) + 2))) >= 0 by INTEGRA1:9;

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, A111, A112, A109, A113, A127, FINSEQ_6:118;

then A134: ((indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, XREAL_1:233;

then A135: (indx (D2,D1,j1)) + 2 in dom D2 by A3, A5, INTEGRA1:def 19;

lower_bound (divset (D1,(len D1))) = D1 . j1 by A5, A7, INTEGRA1:def 4;

then lower_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,j1)) by A3, A8, INTEGRA1:def 19;

then A136: vol (divset (D1,(len D1))) = (((D2 . ((indx (D2,D1,j1)) + 2)) - (D2 . ((indx (D2,D1,j1)) + 1))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A132, A134, INTEGRA1:def 5;

(indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (g,D2))) by A109, A113, FINSEQ_1:1;

then (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

then A137: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;

A138: (indx (D2,D1,j1)) + 1 <> 1 by A14, NAT_1:13;

then A139: upper_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . ((indx (D2,D1,j1)) + 1) by A137, INTEGRA1:def 4;

((indx (D2,D1,j1)) + 1) - 1 = (indx (D2,D1,j1)) + 0 ;

then A140: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A137, A138, INTEGRA1:def 4;

A141: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A109, NAT_1:13;

((indx (D2,D1,j1)) + 2) - 1 = (indx (D2,D1,j1)) + 1 ;

then A142: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A135, A141, INTEGRA1:def 4;

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A135, A141, INTEGRA1:def 4;

then vol (divset (D1,(len D1))) = ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A142, A136, INTEGRA1:def 5

.= (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + ((upper_bound (divset (D2,((indx (D2,D1,j1)) + 1)))) - (lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))))) by A140, A139 ;

then A143: vol (divset (D1,(len D1))) = (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by INTEGRA1:def 5;

then A144: (lower_volume (g,D1)) . (len D1) = (lower_bound (rng (g | (divset (D1,(len D1)))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A5, INTEGRA1:def 7;

A145: (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H_{1}(D1),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))

then ((upper_bound (rng g)) - (lower_bound (rng g))) * (vol (divset (D1,(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A5, Lm5, XREAL_1:64;

hence (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A143, A145, XXREAL_0:2; :: thesis: verum

end;A129: 2 + ((indx (D2,D1,j1)) + 1) >= 0 + 1 by XREAL_1:7;

(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 2 = H

.= H

.= H

then mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))) = <*((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)),((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 2))*> by A127, A128, FINSEQ_1:44;

then A130: Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = ((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)) + ((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 2)) by RVSUM_1:77;

A131: vol (divset (D2,((indx (D2,D1,j1)) + 1))) >= 0 by INTEGRA1:9;

upper_bound (divset (D1,(len D1))) = D1 . (len D1) by A5, A7, INTEGRA1:def 4;

then A132: upper_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,(len D1))) by A3, A5, INTEGRA1:def 19;

A133: vol (divset (D2,((indx (D2,D1,j1)) + 2))) >= 0 by INTEGRA1:9;

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, A111, A112, A109, A113, A127, FINSEQ_6:118;

then A134: ((indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, XREAL_1:233;

then A135: (indx (D2,D1,j1)) + 2 in dom D2 by A3, A5, INTEGRA1:def 19;

lower_bound (divset (D1,(len D1))) = D1 . j1 by A5, A7, INTEGRA1:def 4;

then lower_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,j1)) by A3, A8, INTEGRA1:def 19;

then A136: vol (divset (D1,(len D1))) = (((D2 . ((indx (D2,D1,j1)) + 2)) - (D2 . ((indx (D2,D1,j1)) + 1))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A132, A134, INTEGRA1:def 5;

(indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (g,D2))) by A109, A113, FINSEQ_1:1;

then (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

then A137: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;

A138: (indx (D2,D1,j1)) + 1 <> 1 by A14, NAT_1:13;

then A139: upper_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . ((indx (D2,D1,j1)) + 1) by A137, INTEGRA1:def 4;

((indx (D2,D1,j1)) + 1) - 1 = (indx (D2,D1,j1)) + 0 ;

then A140: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A137, A138, INTEGRA1:def 4;

A141: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A109, NAT_1:13;

((indx (D2,D1,j1)) + 2) - 1 = (indx (D2,D1,j1)) + 1 ;

then A142: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A135, A141, INTEGRA1:def 4;

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A135, A141, INTEGRA1:def 4;

then vol (divset (D1,(len D1))) = ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A142, A136, INTEGRA1:def 5

.= (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + ((upper_bound (divset (D2,((indx (D2,D1,j1)) + 1)))) - (lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))))) by A140, A139 ;

then A143: vol (divset (D1,(len D1))) = (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by INTEGRA1:def 5;

then A144: (lower_volume (g,D1)) . (len D1) = (lower_bound (rng (g | (divset (D1,(len D1)))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A5, INTEGRA1:def 7;

A145: (Sum (mid (H

proof

(upper_bound (rng g)) - (lower_bound (rng g)) >= 0
by A72, Lm3, XREAL_1:48;
set ID1 = (indx (D2,D1,j1)) + 1;

set ID2 = (indx (D2,D1,j1)) + 2;

set IR = (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))));

divset (D1,(len D1)) c= A by A5, INTEGRA1:8;

then A146: lower_bound (rng (g | (divset (D1,(len D1))))) >= lower_bound (rng g) by A72, Lm4;

Sum (mid (H_{1}(D1),(len D1),(len D1))) = ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by A108, A144, FINSOP_1:11;

then (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by A133, A146, XREAL_1:64;

then Sum (mid (H_{1}(D1),(len D1),(len D1))) >= ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) + ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))))
by XREAL_1:19;

then A147: (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:19;

(lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A131, A146, XREAL_1:64;

then (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A147, XXREAL_0:2;

then A148: Sum (mid (H_{1}(D1),(len D1),(len D1))) >= ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:19;

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, A111, A112, A109, A113, A127, FINSEQ_6:118;

then A149: ((indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, XREAL_1:233;

(indx (D2,D1,j1)) + 1 in dom D2 by A114, FINSEQ_1:def 3;

then divset (D2,((indx (D2,D1,j1)) + 1)) c= A by INTEGRA1:8;

then lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1))))) <= upper_bound (rng g) by A72, Lm4;

then A150: (lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A131, XREAL_1:64;

A151: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then divset (D2,((indx (D2,D1,j1)) + 2)) c= A by A149, INTEGRA1:8;

then A152: lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2))))) <= upper_bound (rng g) by A72, Lm4;

Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) =
((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + (H_{1}(D2) . ((indx (D2,D1,j1)) + 1))
by A130, A151, A149, INTEGRA1:def 7

.= ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A116, INTEGRA1:def 7 ;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by A133, A152, XREAL_1:64;

then Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:20;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:20;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A150, XXREAL_0:2;

then Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:20;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H_{1}(D1),(len D1),(len D1)))) <= (((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))) - (((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))))
by A148, XREAL_1:13;

hence (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H_{1}(D1),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
; :: thesis: verum

end;set ID2 = (indx (D2,D1,j1)) + 2;

set IR = (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))));

divset (D1,(len D1)) c= A by A5, INTEGRA1:8;

then A146: lower_bound (rng (g | (divset (D1,(len D1))))) >= lower_bound (rng g) by A72, Lm4;

Sum (mid (H

then (Sum (mid (H

then Sum (mid (H

then A147: (Sum (mid (H

(lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A131, A146, XREAL_1:64;

then (Sum (mid (H

then A148: Sum (mid (H

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, A111, A112, A109, A113, A127, FINSEQ_6:118;

then A149: ((indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A79, XREAL_1:233;

(indx (D2,D1,j1)) + 1 in dom D2 by A114, FINSEQ_1:def 3;

then divset (D2,((indx (D2,D1,j1)) + 1)) c= A by INTEGRA1:8;

then lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1))))) <= upper_bound (rng g) by A72, Lm4;

then A150: (lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A131, XREAL_1:64;

A151: indx (D2,D1,(len D1)) in dom D2 by A3, A5, INTEGRA1:def 19;

then divset (D2,((indx (D2,D1,j1)) + 2)) c= A by A149, INTEGRA1:8;

then A152: lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2))))) <= upper_bound (rng g) by A72, Lm4;

Sum (mid (H

.= ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A116, INTEGRA1:def 7 ;

then (Sum (mid (H

then Sum (mid (H

then (Sum (mid (H

then (Sum (mid (H

then Sum (mid (H

then (Sum (mid (H

hence (Sum (mid (H

then ((upper_bound (rng g)) - (lower_bound (rng g))) * (vol (divset (D1,(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A5, Lm5, XREAL_1:64;

hence (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A143, A145, XXREAL_0:2; :: thesis: verum

then indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;

then A153: indx (D2,D1,j1) <= len (lower_volume (g,D2)) by INTEGRA1:def 7;

j1 <= len D1 by A12, FINSEQ_3:25;

then A154: j1 <= len (lower_volume (g,D1)) by INTEGRA1:def 7;

A155: D2 . (indx (D2,D1,(len D1))) = D1 . (len D1) by A3, A5, INTEGRA1:def 19;

A156: indx (D2,D1,(len D1)) >= len (lower_volume (g,D2))

proof

indx (D2,D1,(len D1)) in Seg (len D2)
by A6, FINSEQ_1:def 3;
assume
indx (D2,D1,(len D1)) < len (lower_volume (g,D2))
; :: thesis: contradiction

then indx (D2,D1,(len D1)) < len D2 by INTEGRA1:def 7;

then A157: D1 . (len D1) < D2 . (len D2) by A66, A6, A155, SEQM_3:def 1;

A158: not D2 . (len D2) in rng D1

then ( D2 . (len D2) in rng D1 or D2 . (len D2) in {x} ) by A4, XBOOLE_0:def 3;

then D2 . (len D2) = x by A158, TARSKI:def 1;

then D2 . (len D2) <= upper_bound (divset (D1,(len D1))) by A1, INTEGRA2:1;

hence contradiction by A5, A7, A157, INTEGRA1:def 4; :: thesis: verum

end;then indx (D2,D1,(len D1)) < len D2 by INTEGRA1:def 7;

then A157: D1 . (len D1) < D2 . (len D2) by A66, A6, A155, SEQM_3:def 1;

A158: not D2 . (len D2) in rng D1

proof

D2 . (len D2) in rng D2
by A66, FUNCT_1:def 3;
assume
D2 . (len D2) in rng D1
; :: thesis: contradiction

D2 . (len D2) <= upper_bound A by INTEGRA1:def 2;

hence contradiction by A157, INTEGRA1:def 2; :: thesis: verum

end;D2 . (len D2) <= upper_bound A by INTEGRA1:def 2;

hence contradiction by A157, INTEGRA1:def 2; :: thesis: verum

then ( D2 . (len D2) in rng D1 or D2 . (len D2) in {x} ) by A4, XBOOLE_0:def 3;

then D2 . (len D2) = x by A158, TARSKI:def 1;

then D2 . (len D2) <= upper_bound (divset (D1,(len D1))) by A1, INTEGRA2:1;

hence contradiction by A5, A7, A157, INTEGRA1:def 4; :: thesis: verum

then indx (D2,D1,(len D1)) in Seg (len (lower_volume (g,D2))) by INTEGRA1:def 7;

then indx (D2,D1,(len D1)) in dom (lower_volume (g,D2)) by FINSEQ_1:def 3;

then A159: H

.= Sum (lower_volume (g,D2)) by A156, FINSEQ_1:58 ;

len D1 in Seg (len (lower_volume (g,D1))) by A69, INTEGRA1:def 7;

then len D1 in dom (lower_volume (g,D1)) by FINSEQ_1:def 3;

then A160: H

.= Sum (lower_volume (g,D1)) by A67, FINSEQ_1:58 ;

len D1 = len (lower_volume (g,D1)) by INTEGRA1:def 7;

then A161: j1 in dom (lower_volume (g,D1)) by A8, FINSEQ_3:29;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A15, A11, A18, Th6;

then indx (D2,D1,j1) = j1 by A9, A17, FINSEQ_1:59;

then len ((lower_volume (g,D1)) | j1) = indx (D2,D1,j1) by A154, FINSEQ_1:59;

then len ((lower_volume (g,D1)) | j1) = len ((lower_volume (g,D2)) | (indx (D2,D1,j1))) by A153, FINSEQ_1:59;

then A162: (lower_volume (g,D2)) | (indx (D2,D1,j1)) = (lower_volume (g,D1)) | j1 by A38, FINSEQ_1:14;

len D2 = len (lower_volume (g,D2)) by INTEGRA1:def 7;

then indx (D2,D1,j1) in dom (lower_volume (g,D2)) by A13, FINSEQ_3:29;

then A163: H

.= H

indx (D2,D1,(len D1)) <= len D2 by A76, FINSEQ_1:1;

then A164: indx (D2,D1,(len D1)) <= len H

A165: len D2 = len H

then A166: indx (D2,D1,(len D1)) in dom H

indx (D2,D1,j1) in dom H

then H

then H

.= Sum ((mid (H

.= Sum (mid (H

.= Sum (H

then H

hence (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A163, A81, A74, A159, A160; :: thesis: verum