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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

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

then A6: len D1 in dom D1 by FINSEQ_1:def 3;

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

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

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

A8: len D1 >= len (upper_volume (g,D1)) by INTEGRA1:def 6;

A9: len D1 <> 1 by A2;

then A10: (len D1) - 1 in dom D1 by A6, INTEGRA1:7;

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

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

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

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

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

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

then j1 < len D1 by XREAL_1:19;

then A14: indx (D2,D1,j1) < indx (D2,D1,(len D1)) by A3, A6, A10, Th8;

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

len D2 in Seg (len D2) by FINSEQ_1:3;

then A16: len D2 in dom D2 by FINSEQ_1:def 3;

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

A18: indx (D2,D1,(len D1)) >= len (upper_volume (g,D2))

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

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

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

.= Sum (upper_volume (g,D2)) by A18, FINSEQ_1:58 ;

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

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

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

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

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

A26: j1 <= len D1 by A10, FINSEQ_3:25;

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

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

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

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

.= Sum (upper_volume (g,D1)) by A8, FINSEQ_1:58 ;

A102: len D1 <= len H_{1}(D1)
by INTEGRA1:def 6;

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

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

then A104: D1 | j1 is increasing by A103, FINSEQ_6:116;

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

then A106: D2 | (indx (D2,D1,j1)) = D1 | j1 by A13, A104, Th6;

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

k = indx (D2,D1,k)

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

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

then A154: indx (D2,D1,j1) <= len (upper_volume (g,D2)) by INTEGRA1:def 6;

j1 in Seg (len D1) by A10, FINSEQ_1:def 3;

then j1 <= len D1 by FINSEQ_1:1;

then A155: j1 <= len (upper_volume (g,D1)) by INTEGRA1:def 6;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A13, A104, A105, Th6;

then indx (D2,D1,j1) = j1 by A26, A25, FINSEQ_1:59;

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

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

then A156: (upper_volume (g,D2)) | (indx (D2,D1,j1)) = (upper_volume (g,D1)) | j1 by A125, FINSEQ_1:14;

j1 in Seg (len D1) by A10, FINSEQ_1:def 3;

then j1 in Seg (len (upper_volume (g,D1))) by INTEGRA1:def 6;

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

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

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

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

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

then A160: indx (D2,D1,(len D1)) in dom H_{1}(D2)
by A23, FINSEQ_3:25;

indx (D2,D1,j1) in Seg (len D2) by A11, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len H_{1}(D2))
by INTEGRA1:def 6;

then indx (D2,D1,j1) in dom H_{1}(D2)
by FINSEQ_1:def 3;

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 ((upper_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 A12, FINSEQ_6:116

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

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

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

A162: 1 <= len D1 by A5, FINSEQ_1:1;

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

j1 in Seg (len D1) by A10, FINSEQ_1:def 3;

then j1 in Seg (len H_{1}(D1))
by INTEGRA1:def 6;

then j1 in dom H_{1}(D1)
by FINSEQ_1:def 3;

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 A103, FINSEQ_6:116

.= Sum (mid (H_{1}(D1),1,(len D1)))
by A103, A102, A158, INTEGRA2:4

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

then A164: H_{2}(D1,j1) + (Sum (mid ((upper_volume (g,D1)),(len D1),(len D1)))) = H_{2}(D1, len D1)
by A163, INTEGRA1:def 20;

indx (D2,D1,j1) in Seg (len D2) by A11, FINSEQ_1:def 3;

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

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

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

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

hence (Sum (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A28, A161, A164, A21, A101; :: 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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((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 (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )

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

then A6: len D1 in dom D1 by FINSEQ_1:def 3;

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

deffunc H

deffunc H

A8: len D1 >= len (upper_volume (g,D1)) by INTEGRA1:def 6;

A9: len D1 <> 1 by A2;

then A10: (len D1) - 1 in dom D1 by A6, INTEGRA1:7;

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

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

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

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

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

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

then j1 < len D1 by XREAL_1:19;

then A14: indx (D2,D1,j1) < indx (D2,D1,(len D1)) by A3, A6, A10, Th8;

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

len D2 in Seg (len D2) by FINSEQ_1:3;

then A16: len D2 in dom D2 by FINSEQ_1:def 3;

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

A18: indx (D2,D1,(len D1)) >= len (upper_volume (g,D2))

proof

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

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

then A19: D1 . (len D1) < D2 . (len D2) by A16, A7, A17, SEQM_3:def 1;

A20: 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 A20, TARSKI:def 1;

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

hence contradiction by A6, A9, A19, INTEGRA1:def 4; :: thesis: verum

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

then A19: D1 . (len D1) < D2 . (len D2) by A16, A7, A17, SEQM_3:def 1;

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

proof

D2 . (len D2) in rng D2
by A16, 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 A19, INTEGRA1:def 2; :: thesis: verum

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

hence contradiction by A19, 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 A20, TARSKI:def 1;

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

hence contradiction by A6, A9, A19, INTEGRA1:def 4; :: thesis: verum

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

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

then A21: H

.= Sum (upper_volume (g,D2)) by A18, FINSEQ_1:58 ;

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

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

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

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

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

A26: j1 <= len D1 by A10, FINSEQ_3:25;

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

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

proof

len D1 in Seg (len (upper_volume (g,D1)))
by A5, INTEGRA1:def 6;
A29:
(indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) <= 2

A53: 1 <= len D1 by A5, FINSEQ_1:1;

then A54: (mid ((upper_volume (g,D1)),(len D1),(len D1))) . 1 = (upper_volume (g,D1)) . (len D1) by A52, FINSEQ_6:118;

reconsider uv = (upper_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 ((upper_volume (g,D1)),(len D1),(len D1))) = 1 by A53, A52, FINSEQ_6:118;

then mid ((upper_volume (g,D1)),(len D1),(len D1)) = <*uv*> by A54, FINSEQ_1:40;

then A55: Sum (mid ((upper_volume (g,D1)),(len D1),(len D1))) = (upper_volume (g,D1)) . (len D1) by FINSOP_1:11;

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

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

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

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

indx (D2,D1,(len D1)) in Seg (len (upper_volume (g,D2))) by A57, INTEGRA1:def 6;

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

then A60: (indx (D2,D1,j1)) + 1 <= len (upper_volume (g,D2)) by A15, XXREAL_0:2;

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

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

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

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

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

then A63: len (mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= 2 by A15, A58, A59, A56, A60, FINSEQ_6:118;

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

then A64: 1 <= len (mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) by A15, A58, A59, A56, A60, FINSEQ_6:118;

end;proof

A52:
len D1 <= len (upper_volume (g,D1))
by INTEGRA1:def 6;
reconsider ID1 = (indx (D2,D1,j1)) + 1 as Element of NAT ;

reconsider ID2 = ID1 + 1 as Element of NAT ;

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

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

A31: ID1 < ID2 by NAT_1:13;

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

then A32: 1 <= ID2 by A12, XXREAL_0:2;

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

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

then ID2 <= len D2 by A30, XXREAL_0:2;

then A35: ID2 in dom D2 by A32, FINSEQ_3:25;

then A36: D2 . ID2 < D2 . (indx (D2,D1,(len D1))) by A30, A33, SEQM_3:def 1;

A37: 1 <= ID1 by A12, NAT_1:13;

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

ID1 <= indx (D2,D1,(len D1)) by A30, A31, XXREAL_0:2;

then ID1 <= len D2 by A34, XXREAL_0:2;

then A39: ID1 in dom D2 by A37, FINSEQ_3:25;

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

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

then A41: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A11, A39, SEQM_3:def 1;

A42: D2 . ID1 < D2 . ID2 by A31, A39, A35, SEQM_3:def 1;

A43: ( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

then D2 . ID1 in {x} by A4, A43, XBOOLE_0:def 3;

then A51: D2 . ID1 = x by TARSKI:def 1;

D2 . ID2 in rng D2 by A35, FUNCT_1:def 3;

then D2 . ID2 in {x} by A4, A43, XBOOLE_0:def 3;

then D2 . ID1 = D2 . ID2 by A51, TARSKI:def 1;

hence contradiction by A31, A39, A35, SEQ_4:138; :: thesis: verum

end;reconsider ID2 = ID1 + 1 as Element of NAT ;

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

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

A31: ID1 < ID2 by NAT_1:13;

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

then A32: 1 <= ID2 by A12, XXREAL_0:2;

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

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

then ID2 <= len D2 by A30, XXREAL_0:2;

then A35: ID2 in dom D2 by A32, FINSEQ_3:25;

then A36: D2 . ID2 < D2 . (indx (D2,D1,(len D1))) by A30, A33, SEQM_3:def 1;

A37: 1 <= ID1 by A12, NAT_1:13;

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

ID1 <= indx (D2,D1,(len D1)) by A30, A31, XXREAL_0:2;

then ID1 <= len D2 by A34, XXREAL_0:2;

then A39: ID1 in dom D2 by A37, FINSEQ_3:25;

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

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

then A41: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A11, A39, SEQM_3:def 1;

A42: D2 . ID1 < D2 . ID2 by A31, A39, A35, SEQM_3:def 1;

A43: ( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

proof

D2 . ID1 in rng D2
by A39, FUNCT_1:def 3;
assume A44:
( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 )
; :: thesis: contradiction

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 )
by A44;

end;

suppose
D2 . ID1 in rng D1
; :: thesis: contradiction

then consider n being Element of NAT such that

A45: n in dom D1 and

A46: D1 . n = D2 . ID1 by PARTFUN1:3;

j1 < n by A10, A41, A38, A45, A46, SEQ_4:137;

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

D2 . ID1 < D2 . (indx (D2,D1,(len D1))) by A42, A36, XXREAL_0:2;

then n < len D1 by A6, A40, A45, A46, SEQ_4:137;

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

end;A45: n in dom D1 and

A46: D1 . n = D2 . ID1 by PARTFUN1:3;

j1 < n by A10, A41, A38, A45, A46, SEQ_4:137;

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

D2 . ID1 < D2 . (indx (D2,D1,(len D1))) by A42, A36, XXREAL_0:2;

then n < len D1 by A6, A40, A45, A46, SEQ_4:137;

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

suppose
D2 . ID2 in rng D1
; :: thesis: contradiction

then consider n being Element of NAT such that

A48: n in dom D1 and

A49: D1 . n = D2 . ID2 by PARTFUN1:3;

D2 . (indx (D2,D1,j1)) < D2 . ID2 by A41, A42, XXREAL_0:2;

then j1 < n by A10, A38, A48, A49, SEQ_4:137;

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

n < len D1 by A6, A36, A40, A48, A49, SEQ_4:137;

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

end;A48: n in dom D1 and

A49: D1 . n = D2 . ID2 by PARTFUN1:3;

D2 . (indx (D2,D1,j1)) < D2 . ID2 by A41, A42, XXREAL_0:2;

then j1 < n by A10, A38, A48, A49, SEQ_4:137;

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

n < len D1 by A6, A36, A40, A48, A49, SEQ_4:137;

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

then D2 . ID1 in {x} by A4, A43, XBOOLE_0:def 3;

then A51: D2 . ID1 = x by TARSKI:def 1;

D2 . ID2 in rng D2 by A35, FUNCT_1:def 3;

then D2 . ID2 in {x} by A4, A43, XBOOLE_0:def 3;

then D2 . ID1 = D2 . ID2 by A51, TARSKI:def 1;

hence contradiction by A31, A39, A35, SEQ_4:138; :: thesis: verum

A53: 1 <= len D1 by A5, FINSEQ_1:1;

then A54: (mid ((upper_volume (g,D1)),(len D1),(len D1))) . 1 = (upper_volume (g,D1)) . (len D1) by A52, FINSEQ_6:118;

reconsider uv = (upper_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 ((upper_volume (g,D1)),(len D1),(len D1))) = 1 by A53, A52, FINSEQ_6:118;

then mid ((upper_volume (g,D1)),(len D1),(len D1)) = <*uv*> by A54, FINSEQ_1:40;

then A55: Sum (mid ((upper_volume (g,D1)),(len D1),(len D1))) = (upper_volume (g,D1)) . (len D1) by FINSOP_1:11;

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

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

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

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

indx (D2,D1,(len D1)) in Seg (len (upper_volume (g,D2))) by A57, INTEGRA1:def 6;

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

then A60: (indx (D2,D1,j1)) + 1 <= len (upper_volume (g,D2)) by A15, XXREAL_0:2;

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

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

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

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

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

then A63: len (mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= 2 by A15, A58, A59, A56, A60, FINSEQ_6:118;

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

then A64: 1 <= len (mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) by A15, A58, A59, A56, A60, FINSEQ_6:118;

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

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

end;

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

upper_bound (divset (D1,(len D1))) = D1 . (len D1)
by A6, A9, INTEGRA1:def 4;

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

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

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

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

A68: delta D1 >= 0 by Th9;

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

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

len (mid ((upper_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 A15, A58, A59, A56, A60, FINSEQ_6:118;

then A71: (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) = 0 by A15, A65, XREAL_1:233;

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

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

lower_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . ((indx (D2,D1,(len D1))) - 1) by A12, A71, A70, INTEGRA1:def 4;

then A73: divset (D2,(indx (D2,D1,(len D1)))) = divset (D1,(len D1)) by A71, A67, A72, INTEGRA1:4;

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

(mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1 = (upper_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) by A58, A59, A56, A60, FINSEQ_6:118;

then mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))) = <*uv*> by A65, FINSEQ_1:40;

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

.= (upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A62, INTEGRA1:def 6

.= Sum (mid ((upper_volume (g,D1)),(len D1),(len D1))) by A6, A55, A71, A73, INTEGRA1:def 6 ;

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

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

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

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

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

A68: delta D1 >= 0 by Th9;

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

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

len (mid ((upper_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 A15, A58, A59, A56, A60, FINSEQ_6:118;

then A71: (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) = 0 by A15, A65, XREAL_1:233;

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

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

lower_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . ((indx (D2,D1,(len D1))) - 1) by A12, A71, A70, INTEGRA1:def 4;

then A73: divset (D2,(indx (D2,D1,(len D1)))) = divset (D1,(len D1)) by A71, A67, A72, INTEGRA1:4;

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

(mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1 = (upper_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) by A58, A59, A56, A60, FINSEQ_6:118;

then mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))) = <*uv*> by A65, FINSEQ_1:40;

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

.= (upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A62, INTEGRA1:def 6

.= Sum (mid ((upper_volume (g,D1)),(len D1),(len D1))) by A6, A55, A71, A73, INTEGRA1:def 6 ;

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

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

A75:
(mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1 = (upper_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)
by A58, A59, A56, A60, FINSEQ_6:118;

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

(mid ((upper_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 A15, A58, A59, A56, A60, A74, FINSEQ_6:118

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

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

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

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

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

upper_bound (divset (D1,(len D1))) = D1 . (len D1) by A6, A9, INTEGRA1:def 4;

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

A80: 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 A15, A58, A59, A56, A60, A74, FINSEQ_6:118;

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

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

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

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

then A83: 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 A79, A81, INTEGRA1:def 5;

(indx (D2,D1,j1)) + 1 in Seg (len (upper_volume (g,D2))) by A56, A60, FINSEQ_1:1;

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

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

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

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

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

then A87: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A84, A85, INTEGRA1:def 4;

A88: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A56, NAT_1:13;

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

then A89: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A82, A88, INTEGRA1:def 4;

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A82, A88, 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 A89, A83, 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 A87, A86 ;

then A90: 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 A91: (upper_volume (g,D1)) . (len D1) = (upper_bound (rng (g | (divset (D1,(len D1)))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A6, INTEGRA1:def 6;

A92: (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,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 A6, Lm5, XREAL_1:64;

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

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

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

.= H

.= H

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

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

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

upper_bound (divset (D1,(len D1))) = D1 . (len D1) by A6, A9, INTEGRA1:def 4;

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

A80: 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 A15, A58, A59, A56, A60, A74, FINSEQ_6:118;

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

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

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

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

then A83: 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 A79, A81, INTEGRA1:def 5;

(indx (D2,D1,j1)) + 1 in Seg (len (upper_volume (g,D2))) by A56, A60, FINSEQ_1:1;

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

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

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

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

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

then A87: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A84, A85, INTEGRA1:def 4;

A88: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A56, NAT_1:13;

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

then A89: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A82, A88, INTEGRA1:def 4;

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A82, A88, 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 A89, A83, 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 A87, A86 ;

then A90: 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 A91: (upper_volume (g,D1)) . (len D1) = (upper_bound (rng (g | (divset (D1,(len D1)))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A6, INTEGRA1:def 6;

A92: (Sum (mid (H

proof

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

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

A93: (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - ((upper_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = (upper_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by A55, A91;

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

then A94: upper_bound (rng (g | (divset (D1,(len D1))))) <= upper_bound (rng g) by A27, Lm4;

then (upper_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A80, XREAL_1:64;

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

then A95: (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 | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:20;

(upper_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A78, A94, XREAL_1:64;

then (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))))
by A95, XXREAL_0:2;

then A96: 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)))))
by XREAL_1:20;

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

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

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

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

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A15, A58, A59, A56, A60, A74, FINSEQ_6:118;

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

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

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

then A100: upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2))))) >= lower_bound (rng g) by A27, Lm4;

Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) =
((upper_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 A77, A99, A98, INTEGRA1:def 6

.= ((upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A62, INTEGRA1:def 6 ;

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

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

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

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,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 A97, XXREAL_0:2;

then Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,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;

then (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - (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)))))) - (((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 A96, XREAL_1:13;

hence (Sum (mid (H_{1}(D1),(len D1),(len D1)))) - (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,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;

A93: (Sum (mid (H

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

then A94: upper_bound (rng (g | (divset (D1,(len D1))))) <= upper_bound (rng g) by A27, Lm4;

then (upper_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A80, XREAL_1:64;

then Sum (mid (H

then A95: (Sum (mid (H

(upper_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A78, A94, XREAL_1:64;

then (Sum (mid (H

then A96: Sum (mid (H

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

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

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

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

((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A15, A58, A59, A56, A60, A74, FINSEQ_6:118;

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

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

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

then A100: upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2))))) >= lower_bound (rng g) by A27, Lm4;

Sum (mid (H

.= ((upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A62, INTEGRA1:def 6 ;

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 A6, Lm5, XREAL_1:64;

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

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

then A101: H

.= Sum (upper_volume (g,D1)) by A8, FINSEQ_1:58 ;

A102: len D1 <= len H

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

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

then A104: D1 | j1 is increasing by A103, FINSEQ_6:116;

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

then A106: D2 | (indx (D2,D1,j1)) = D1 | j1 by A13, A104, Th6;

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

k = indx (D2,D1,k)

proof

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

assume that

A108: 1 <= k and

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

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

end;assume that

A108: 1 <= k and

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

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

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k > indx (D2,D1,k) or k < indx (D2,D1,k) )
by A110, XXREAL_0:1;

end;

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

k <= len D1
by A26, A109, XXREAL_0:2;

then A112: k in dom D1 by A108, 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 A113: 1 <= indx (D2,D1,k) by FINSEQ_1:1;

A114: indx (D2,D1,k) < j1 by A109, A111, XXREAL_0:2;

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

indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A10, A109, A112, Th7;

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

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

indx (D2,D1,k) <= len D1 by A26, A114, XXREAL_0:2;

then indx (D2,D1,k) in Seg (len D1) by A113, FINSEQ_1:1;

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

then A117: D1 . k > D1 . (indx (D2,D1,k)) by A111, A112, SEQM_3:def 1;

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

hence contradiction by A10, A106, A116, A117, A115, RFINSEQ:6; :: thesis: verum

end;then A112: k in dom D1 by A108, 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 A113: 1 <= indx (D2,D1,k) by FINSEQ_1:1;

A114: indx (D2,D1,k) < j1 by A109, A111, XXREAL_0:2;

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

indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A10, A109, A112, Th7;

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

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

indx (D2,D1,k) <= len D1 by A26, A114, XXREAL_0:2;

then indx (D2,D1,k) in Seg (len D1) by A113, FINSEQ_1:1;

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

then A117: D1 . k > D1 . (indx (D2,D1,k)) by A111, A112, SEQM_3:def 1;

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

hence contradiction by A10, A106, A116, A117, A115, RFINSEQ:6; :: thesis: verum

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

k <= len D1
by A26, A109, XXREAL_0:2;

then A119: k in dom D1 by A108, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A10, A109, Th7;

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

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

then A121: k in dom D2 by A108, FINSEQ_3:25;

k in Seg j1 by A108, A109, FINSEQ_1:1;

then A122: D1 . k = (D1 | j1) . k by A10, RFINSEQ:6;

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

then A123: D2 . k < D2 . (indx (D2,D1,k)) by A118, A121, SEQM_3:def 1;

A124: k in Seg (indx (D2,D1,j1)) by A108, A120, FINSEQ_1:1;

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

hence contradiction by A11, A106, A122, A123, A124, RFINSEQ:6; :: thesis: verum

end;then A119: k in dom D1 by A108, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A3, A10, A109, Th7;

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

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

then A121: k in dom D2 by A108, FINSEQ_3:25;

k in Seg j1 by A108, A109, FINSEQ_1:1;

then A122: D1 . k = (D1 | j1) . k by A10, RFINSEQ:6;

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

then A123: D2 . k < D2 . (indx (D2,D1,k)) by A118, A121, SEQM_3:def 1;

A124: k in Seg (indx (D2,D1,j1)) by A108, A120, FINSEQ_1:1;

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

hence contradiction by A11, A106, A122, A123, A124, RFINSEQ:6; :: thesis: verum

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

proof

indx (D2,D1,j1) in dom D2
by A3, A10, INTEGRA1:def 19;
indx (D2,D1,j1) in Seg (len D2)
by A11, FINSEQ_1:def 3;

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

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

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

assume that

A127: 1 <= k and

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

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

A129: len (upper_volume (g,D1)) = len D1 by INTEGRA1:def 6;

then A130: k <= j1 by A26, A128, FINSEQ_1:59;

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

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

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

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

A134: k in Seg j1 by A127, A130, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A107, A127, A130;

then A135: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A103, A107;

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

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

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

A138: ( 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 A150: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A138, INTEGRA1:4;

A151: k in dom D1 by A127, A131, FINSEQ_3:25;

j1 in Seg (len (upper_volume (g,D1))) by A10, A129, FINSEQ_1:def 3;

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

then A152: ((upper_volume (g,D1)) | j1) . k = (upper_volume (g,D1)) . k by A134, RFINSEQ:6

.= (upper_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A151, A150, INTEGRA1:def 6 ;

1 <= indx (D2,D1,k) by A107, A127, A130;

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

((upper_volume (g,D2)) | (indx (D2,D1,j1))) . k = ((upper_volume (g,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A107, A127, A130

.= (upper_volume (g,D2)) . (indx (D2,D1,k)) by A135, A126, RFINSEQ:6

.= (upper_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A153, INTEGRA1:def 6 ;

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

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

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

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

assume that

A127: 1 <= k and

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

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

A129: len (upper_volume (g,D1)) = len D1 by INTEGRA1:def 6;

then A130: k <= j1 by A26, A128, FINSEQ_1:59;

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

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

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

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

A134: k in Seg j1 by A127, A130, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A107, A127, A130;

then A135: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A103, A107;

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

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

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

A138: ( 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 A139:
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 A140:
upper_bound (divset (D1,k)) = D1 . k
by A132, INTEGRA1:def 4;

A141: lower_bound (divset (D1,k)) = lower_bound A by A132, A139, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A103, A107, A139;

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 A133, A137, A141, A140, INTEGRA1:def 4; :: thesis: verum

end;A141: lower_bound (divset (D1,k)) = lower_bound A by A132, A139, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A103, A107, A139;

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 A133, A137, A141, A140, INTEGRA1:def 4; :: thesis: verum

suppose A142:
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 A132, INTEGRA1:7;

k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A143: k1 <= j1 by A130, XXREAL_0:2;

A144: k - 1 in dom D1 by A132, A142, INTEGRA1:7;

then 1 <= k1 by FINSEQ_3:25;

then k1 = indx (D2,D1,k1) by A107, A143;

then A145: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A107, A127, A130;

A146: indx (D2,D1,k) <> 1 by A107, A127, A130, A142;

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

A148: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A133, A146, INTEGRA1:def 4;

A149: upper_bound (divset (D1,k)) = D1 . k by A132, A142, INTEGRA1:def 4;

lower_bound (divset (D1,k)) = D1 . (k - 1) by A132, A142, INTEGRA1:def 4;

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, A132, A149, A144, A147, A148, A145, INTEGRA1:def 19; :: thesis: verum

end;k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A143: k1 <= j1 by A130, XXREAL_0:2;

A144: k - 1 in dom D1 by A132, A142, INTEGRA1:7;

then 1 <= k1 by FINSEQ_3:25;

then k1 = indx (D2,D1,k1) by A107, A143;

then A145: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A107, A127, A130;

A146: indx (D2,D1,k) <> 1 by A107, A127, A130, A142;

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

A148: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A133, A146, INTEGRA1:def 4;

A149: upper_bound (divset (D1,k)) = D1 . k by A132, A142, INTEGRA1:def 4;

lower_bound (divset (D1,k)) = D1 . (k - 1) by A132, A142, INTEGRA1:def 4;

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, A132, A149, A144, A147, A148, A145, INTEGRA1:def 19; :: thesis: verum

then A150: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A138, INTEGRA1:4;

A151: k in dom D1 by A127, A131, FINSEQ_3:25;

j1 in Seg (len (upper_volume (g,D1))) by A10, A129, FINSEQ_1:def 3;

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

then A152: ((upper_volume (g,D1)) | j1) . k = (upper_volume (g,D1)) . k by A134, RFINSEQ:6

.= (upper_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A151, A150, INTEGRA1:def 6 ;

1 <= indx (D2,D1,k) by A107, A127, A130;

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

((upper_volume (g,D2)) | (indx (D2,D1,j1))) . k = ((upper_volume (g,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A107, A127, A130

.= (upper_volume (g,D2)) . (indx (D2,D1,k)) by A135, A126, RFINSEQ:6

.= (upper_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A153, INTEGRA1:def 6 ;

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

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

then A154: indx (D2,D1,j1) <= len (upper_volume (g,D2)) by INTEGRA1:def 6;

j1 in Seg (len D1) by A10, FINSEQ_1:def 3;

then j1 <= len D1 by FINSEQ_1:1;

then A155: j1 <= len (upper_volume (g,D1)) by INTEGRA1:def 6;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A13, A104, A105, Th6;

then indx (D2,D1,j1) = j1 by A26, A25, FINSEQ_1:59;

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

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

then A156: (upper_volume (g,D2)) | (indx (D2,D1,j1)) = (upper_volume (g,D1)) | j1 by A125, FINSEQ_1:14;

j1 in Seg (len D1) by A10, FINSEQ_1:def 3;

then j1 in Seg (len (upper_volume (g,D1))) by INTEGRA1:def 6;

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

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

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

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

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

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

indx (D2,D1,j1) in Seg (len D2) by A11, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len H

then indx (D2,D1,j1) in dom H

then H

then H

.= Sum ((mid (H

.= Sum (mid (H

.= Sum (H

then A161: H

A162: 1 <= len D1 by A5, FINSEQ_1:1;

then A163: len D1 in dom H

j1 in Seg (len D1) by A10, FINSEQ_1:def 3;

then j1 in Seg (len H

then j1 in dom H

then H

then H

.= Sum ((mid (H

.= Sum (mid (H

.= Sum (H

then A164: H

indx (D2,D1,j1) in Seg (len D2) by A11, FINSEQ_1:def 3;

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

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

then H

.= H

hence (Sum (upper_volume (g,D1))) - (Sum (upper_volume (g,D2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A28, A161, A164, A21, A101; :: thesis: verum