let x be Real; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let D1, D2 be Division of A; :: thesis:
let g be Function of A,REAL; :: thesis:
assume that
A1: x in divset (D1,(len D1)) and
A2: len D1 >= 2 ; :: thesis:
set j = len D1;
assume that
A3: D1 <= D2 and
A4: rng D2 = (rng D1) \/ {x} ; :: thesis:
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

let k be Element of NAT ; :: thesis:
assume that
A21: 1 <= k and
A22: k <= j1 ; :: thesis:
assume A23: k <> indx (D2,D1,k) ; :: thesis:

per cases by A23, XXREAL_0:1;

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

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:

end;

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

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:

end;

A38: for k being Nat st 1 <= k & k <= len ((lower_volume (g,D1)) | j1) holds
((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k

proof

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:
assume that
A40: 1 <= k and
A41: k <= len ((lower_volume (g,D1)) | j1) ; :: thesis:
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

per cases ;

suppose A51: k = 1 ; :: thesis:

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:

end;

suppose A54: k <> 1 ; :: thesis:

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:

end;

divset (D1,k) = [.(lower_bound (divset (D1,k))),(upper_bound (divset (D1,k))).] by INTEGRA1:4;
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:

end;

A66: len D2 in dom D2 by FINSEQ_5:6;
deffunc H₁( Division of A) -> FinSequence of REAL = lower_volume (g,$1);
deffunc H₂( 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₁(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₁(D1) by A68, FINSEQ_3:25;
assume A72: g | A is bounded ; :: thesis:
len D1 < (len D1) + 1 by NAT_1:13;
then A73: j1 < len D1 by XREAL_1:19;
then j1 < len H₁(D1) by INTEGRA1:def 7;
then j1 in dom H₁(D1) by A10, FINSEQ_3:25;
then H₂(D1,j1) = Sum (H₁(D1) | j1) by INTEGRA1:def 20;
then H₂(D1,j1) + (Sum (mid (H₁(D1),(len D1),(len D1)))) = Sum ((H₁(D1) | j1) ^ (mid (H₁(D1),(len D1),(len D1)))) by RVSUM_1:75
.= Sum ((mid (H₁(D1),1,j1)) ^ (mid (H₁(D1),(j1 + 1),(len D1)))) by A10, FINSEQ_6:116
.= Sum (mid (H₁(D1),1,(len D1))) by A10, A68, A73, INTEGRA2:4
.= Sum (H₁(D1) | (len D1)) by A70, FINSEQ_6:116 ;
then A74: H₂(D1,j1) + (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) = H₂(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)

proof

A82: (indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) <= 2

proof

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:
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

assume A97: ( D2 . ((indx (D2,D1,j1)) + 1) in rng D1 or D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 ) ; :: thesis:

per cases by A97;

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

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:

end;

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

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:

end;

D2 . ((indx (D2,D1,j1)) + 1) in rng D2 by A92, FUNCT_1:def 3;
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:

end;

now :: thesis:

per cases by A117, A115, Lm2;

suppose A118: len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 1 ; :: thesis:

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:

end;

suppose A127: len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 2 ; :: thesis:

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₁(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1) by A79, A111, A112, A109, A113, A127, FINSEQ_6:118
.= H₁(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) - 1) by A129, XREAL_1:233
.= H₁(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₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H₁(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)))))

proof

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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H₁(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₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H₁(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:

end;

(upper_bound (rng g)) - (lower_bound (rng g)) >= 0 by A72, Lm3, XREAL_1:48;
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:

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:

end;

indx (D2,D1,j1) in dom D2 by A3, A12, INTEGRA1:def 19;
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

assume indx (D2,D1,(len D1)) < len (lower_volume (g,D2)) ; :: thesis:
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

assume D2 . (len D2) in rng D1 ; :: thesis:
D2 . (len D2) <= upper_bound A by INTEGRA1:def 2;
hence contradiction by A157, INTEGRA1:def 2; :: thesis:

end;

D2 . (len D2) in rng D2 by A66, FUNCT_1:def 3;
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:

end;

indx (D2,D1,(len D1)) in Seg (len D2) by A6, FINSEQ_1:def 3;
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₂(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₂(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₂(D2, indx (D2,D1,j1)) = Sum ((lower_volume (g,D2)) | (indx (D2,D1,j1))) by INTEGRA1:def 20
.= H₂(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₁(D2) by INTEGRA1:def 7;
A165: len D2 = len H₁(D2) by INTEGRA1:def 7;
then A166: indx (D2,D1,(len D1)) in dom H₁(D2) by A75, FINSEQ_3:29;
indx (D2,D1,j1) in dom H₁(D2) by A13, A165, FINSEQ_3:29;
then H₂(D2, indx (D2,D1,j1)) = Sum (H₁(D2) | (indx (D2,D1,j1))) by INTEGRA1:def 20;
then H₂(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) = Sum ((H₁(D2) | (indx (D2,D1,j1))) ^ (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) by RVSUM_1:75
.= Sum ((mid (H₁(D2),1,(indx (D2,D1,j1)))) ^ (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) by A14, FINSEQ_6:116
.= Sum (mid (H₁(D2),1,(indx (D2,D1,(len D1))))) by A14, A78, A164, INTEGRA2:4
.= Sum (H₁(D2) | (indx (D2,D1,(len D1)))) by A77, FINSEQ_6:116 ;
then H₂(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) = H₂(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: