let x be Real; :: thesis:
let A be closed-interval Subset of REAL ; :: thesis:
let D1, D2 be Division of A; :: thesis:
let g be Function of A,REAL ; :: thesis:
assume A1: ( x in divset D1,(len D1) & len D1 >= 2 ) ; :: thesis:
assume A2: ( D1 <= D2 & rng D2 = (rng D1) \/ {x} ) ; :: thesis:
assume A3: g | A is bounded ; :: thesis:
deffunc H₁( Division of A, Nat) -> Element of REAL = (PartSums (lower_volume g,$1)) . $2;
deffunc H₂( Division of A) -> FinSequence of REAL = lower_volume g,$1;
set j = len D1;
A5: ( len D1 in Seg (len D1) & len D2 in Seg (len D2) ) by FINSEQ_1:5;
A6: ( len D1 in dom D1 & len D2 in dom D2 ) by FINSEQ_5:6;
A7: len D1 <> 1 by A1;
A8: ( indx D2,D1,(len D1) in dom D2 & D2 . (indx D2,D1,(len D1)) = D1 . (len D1) ) by A2, A6, INTEGRA1:def 21;
then A9: indx D2,D1,(len D1) in Seg (len D2) by FINSEQ_1:def 3;
A10: 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 8;
then A11: D1 . (len D1) < D2 . (len D2) by A6, A8, SEQM_3:def 1;
A12: not D2 . (len D2) in rng D1

proof

assume A13: D2 . (len D2) in rng D1 ; :: thesis:
rng D1 c= A by INTEGRA1:def 2;
then ( lower_bound A <= D2 . (len D2) & D2 . (len D2) <= upper_bound A ) by A13, INTEGRA2:1;
hence contradiction by A11, INTEGRA1:def 2; :: thesis:

end;

D2 . (len D2) in rng D2 by A6, FUNCT_1:def 5;
then ( D2 . (len D2) in rng D1 or D2 . (len D2) in {x} ) by A2, XBOOLE_0:def 3;
then D2 . (len D2) = x by A12, TARSKI:def 1;
then D2 . (len D2) <= upper_bound (divset D1,(len D1)) by A1, INTEGRA2:1;
hence contradiction by A6, A7, A11, INTEGRA1:def 5; :: thesis:

end;

then A14: ( indx D2,D1,(len D1) in Seg (len (lower_volume g,D2)) & indx D2,D1,(len D1) >= len (lower_volume g,D2) ) by A9, INTEGRA1:def 8;
A15: ( len D1 in Seg (len (lower_volume g,D1)) & len D1 >= len (lower_volume g,D1) ) by A5, INTEGRA1:def 8;
A16: ( (len D1) - 1 in NAT & (len D1) - 1 in dom D1 ) by A6, A7, INTEGRA1:9;
reconsider j1 = (len D1) - 1 as Element of NAT by A6, A7, INTEGRA1:9;
A17: ( indx D2,D1,j1 in dom D2 & 1 <= indx D2,D1,j1 & indx D2,D1,j1 <= len D2 )

proof

thus indx D2,D1,j1 in dom D2 by A2, A16, INTEGRA1:def 21; :: thesis:
hence ( 1 <= indx D2,D1,j1 & indx D2,D1,j1 <= len D2 ) by FINSEQ_3:27; :: thesis:

end;

then mid D2,1,(indx D2,D1,j1) is increasing by INTEGRA1:37;
then A18: D2 | (indx D2,D1,j1) is increasing by A17, JORDAN3:25;
A19: ( j1 in dom D1 & 1 <= j1 & j1 <= len D1 )

proof

thus j1 in dom D1 by A6, A7, INTEGRA1:9; :: thesis:
hence ( 1 <= j1 & j1 <= len D1 ) by FINSEQ_3:27; :: thesis:

end;

then mid D1,1,j1 is increasing by INTEGRA1:37;
then A20: D1 | j1 is increasing by A19, JORDAN3:25;
A21: rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1) by A1, A2, Lm7;
then A22: D2 | (indx D2,D1,j1) = D1 | j1 by A18, A20, Th5;
A23: 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 A24: ( 1 <= k & k <= j1 ) ; :: thesis:
assume A25: k <> indx D2,D1,k ; :: thesis:

per cases by A25, XXREAL_0:1;

suppose A26: k > indx D2,D1,k ; :: thesis:

( 1 <= k & k <= len D1 ) by A19, A24, XXREAL_0:2;
then A27: k in dom D1 by FINSEQ_3:27;
then A28: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A2, INTEGRA1:def 21;
then indx D2,D1,k in Seg (len D2) by FINSEQ_1:def 3;
then A29: ( 1 <= indx D2,D1,k & indx D2,D1,k <= indx D2,D1,j1 ) by A2, A19, A24, A27, Th6, FINSEQ_1:3;
then indx D2,D1,k in Seg (indx D2,D1,j1) by FINSEQ_1:3;
then A30: (D2 | (indx D2,D1,j1)) . (indx D2,D1,k) = D2 . (indx D2,D1,k) by A17, RFINSEQ:19;
A31: indx D2,D1,k < j1 by A24, A26, XXREAL_0:2;
then indx D2,D1,k <= len D1 by A19, XXREAL_0:2;
then indx D2,D1,k in dom D1 by A29, FINSEQ_3:27;
then A32: D1 . k > D1 . (indx D2,D1,k) by A26, A27, SEQM_3:def 1;
indx D2,D1,k in Seg j1 by A29, A31, FINSEQ_1:3;
hence contradiction by A19, A22, A28, A30, A32, RFINSEQ:19; :: thesis:

end;

suppose A33: k < indx D2,D1,k ; :: thesis:

k in Seg j1 by A24, FINSEQ_1:3;
then A34: D1 . k = (D1 | j1) . k by A16, RFINSEQ:19;
( 1 <= k & k <= len D1 ) by A19, A24, XXREAL_0:2;
then A35: k in dom D1 by FINSEQ_3:27;
then A36: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A2, INTEGRA1:def 21;
( indx D2,D1,k <= indx D2,D1,j1 & indx D2,D1,k in dom D2 & indx D2,D1,j1 in dom D2 ) by A2, A19, A24, A35, Th6;
then A37: k <= indx D2,D1,j1 by A33, XXREAL_0:2;
then k <= len D2 by A17, XXREAL_0:2;
then k in dom D2 by A24, FINSEQ_3:27;
then A38: D2 . k < D2 . (indx D2,D1,k) by A33, A36, SEQM_3:def 1;
k in Seg (indx D2,D1,j1) by A24, A37, FINSEQ_1:3;
hence contradiction by A17, A22, A34, A36, A38, RFINSEQ:19; :: thesis:

end;

A39: len (D2 | (indx D2,D1,j1)) = len (D1 | j1) by A18, A20, A21, Th5;
len (D2 | (indx D2,D1,j1)) = indx D2,D1,j1 by A17, FINSEQ_1:80;
then A40: indx D2,D1,j1 = j1 by A19, A39, FINSEQ_1:80;
j1 <= len D1 by A16, FINSEQ_3:27;
then j1 <= len (lower_volume g,D1) by INTEGRA1:def 8;
then A41: len ((lower_volume g,D1) | j1) = indx D2,D1,j1 by A40, FINSEQ_1:80;
indx D2,D1,j1 in dom D2 by A2, A16, INTEGRA1:def 21;
then indx D2,D1,j1 <= len D2 by FINSEQ_3:27;
then indx D2,D1,j1 <= len (lower_volume g,D2) by INTEGRA1:def 8;
then A42: len ((lower_volume g,D1) | j1) = len ((lower_volume g,D2) | (indx D2,D1,j1)) by A41, FINSEQ_1:80;
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

let k be Nat; :: thesis:
assume A43: ( 1 <= k & k <= len ((lower_volume g,D1) | j1) ) ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A44: len (lower_volume g,D1) = len D1 by INTEGRA1:def 8;
then A45: ( 1 <= k & k <= j1 ) by A19, A43, FINSEQ_1:80;
then A46: k in Seg j1 by FINSEQ_1:3;
k <= len D1 by A19, A45, XXREAL_0:2;
then A47: k in Seg (len D1) by A43, FINSEQ_1:3;
A50: k in dom D1 by A47, FINSEQ_1:def 3;
then A51: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A2, INTEGRA1:def 21;
A48: divset D1,k = divset D2,(indx D2,D1,k)

proof

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

then A53: ( lower_bound (divset D1,k) = lower_bound A & upper_bound (divset D1,k) = D1 . k ) by A50, INTEGRA1:def 5;
indx D2,D1,k = 1 by A19, A23, A52;
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 A51, A53, INTEGRA1:def 5; :: thesis:

end;

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

then A55: ( lower_bound (divset D1,k) = D1 . (k - 1) & upper_bound (divset D1,k) = D1 . k ) by A50, INTEGRA1:def 5;
A56: ( k - 1 in dom D1 & D1 . (k - 1) in A & k - 1 in NAT ) by A50, A54, INTEGRA1:9;
reconsider k1 = k - 1 as Element of NAT by A50, A54, INTEGRA1:9;
k <= k + 1 by NAT_1:11;
then k1 <= k by XREAL_1:22;
then A57: k1 <= j1 by A45, XXREAL_0:2;
A58: 1 <= k1 by A56, FINSEQ_3:27;
indx D2,D1,k <> 1 by A23, A45, A54;
then A59: ( lower_bound (divset D2,(indx D2,D1,k)) = D2 . ((indx D2,D1,k) - 1) & upper_bound (divset D2,(indx D2,D1,k)) = D2 . (indx D2,D1,k) ) by A51, INTEGRA1:def 5;
D2 . ((indx D2,D1,k) - 1) = D2 . (k - 1) by A23, A45
.= D2 . (indx D2,D1,k1) by A23, A57, A58 ;
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 A2, A50, A55, A56, A59, INTEGRA1:def 21; :: thesis:

end;

hence divset D1,k = divset D2,(indx D2,D1,k) by A49, INTEGRA1:5; :: thesis:

end;

j1 in Seg (len (lower_volume g,D1)) by A19, A44, FINSEQ_1:def 3;
then j1 in dom (lower_volume g,D1) by FINSEQ_1:def 3;
then A60: ((lower_volume g,D1) | j1) . k = (lower_volume g,D1) . k by A46, RFINSEQ:19
.= (lower_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by A48, A50, INTEGRA1:def 8 ;
indx D2,D1,k in Seg j1 by A23, A45, A46;
then A61: indx D2,D1,k in Seg (indx D2,D1,j1) by A19, A23;
then ( 1 <= indx D2,D1,k & indx D2,D1,k <= indx D2,D1,j1 ) by FINSEQ_1:3;
then Y: ( 1 <= indx D2,D1,k & indx D2,D1,k <= len D2 ) by A17, XXREAL_0:2;
X: indx D2,D1,k in dom D2 by Y, FINSEQ_3:27;
indx D2,D1,j1 in Seg (len D2) by A17, FINSEQ_1:def 3;
then indx D2,D1,j1 in Seg (len (lower_volume g,D2)) by INTEGRA1:def 8;
then A63: indx D2,D1,j1 in dom (lower_volume g,D2) by FINSEQ_1:def 3;
((lower_volume g,D2) | (indx D2,D1,j1)) . k = ((lower_volume g,D2) | (indx D2,D1,j1)) . (indx D2,D1,k) by A23, A45
.= (lower_volume g,D2) . (indx D2,D1,k) by A61, A63, RFINSEQ:19
.= (lower_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by X, INTEGRA1:def 8 ;
hence ((lower_volume g,D1) | j1) . k = ((lower_volume g,D2) | (indx D2,D1,j1)) . k by A60; :: thesis:

end;

then A64: (lower_volume g,D2) | (indx D2,D1,j1) = (lower_volume g,D1) | j1 by A42, FINSEQ_1:18;
X: len D2 = len (lower_volume g,D2) by INTEGRA1:def 8;
B65: indx D2,D1,j1 in dom (lower_volume g,D2) by X, A17, FINSEQ_3:31;
len D1 = len (lower_volume g,D1) by INTEGRA1:def 8;
then Y: j1 in dom (lower_volume g,D1) by A19, FINSEQ_3:31;
A67: H₁(D2, indx D2,D1,j1) = Sum ((lower_volume g,D2) | (indx D2,D1,j1)) by B65, INTEGRA1:def 22
.= H₁(D1,j1) by A64, Y, INTEGRA1:def 22 ;
A68: (indx D2,D1,j1) + 1 <= indx D2,D1,(len D1)

proof

len D1 < (len D1) + 1 by NAT_1:13;
then j1 < len D1 by XREAL_1:21;
then indx D2,D1,j1 < indx D2,D1,(len D1) by A2, A6, A19, Th7;
hence (indx D2,D1,j1) + 1 <= indx D2,D1,(len D1) by NAT_1:13; :: thesis:

end;

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

A70: ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len (lower_volume g,D2) )

proof

indx D2,D1,(len D1) in dom D2 by A2, A6, INTEGRA1:def 21;
then indx D2,D1,(len D1) in Seg (len D2) by FINSEQ_1:def 3;
then indx D2,D1,(len D1) in Seg (len (lower_volume g,D2)) by INTEGRA1:def 8;
hence ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len (lower_volume g,D2) ) by FINSEQ_1:3; :: thesis:

end;

then A71: ( 1 <= (indx D2,D1,j1) + 1 & (indx D2,D1,j1) + 1 <= len (lower_volume g,D2) ) by A17, A68, NAT_1:13, XXREAL_0:2;
A72: (indx D2,D1,(len D1)) - (indx D2,D1,j1) <= 2

proof

assume A73: (indx D2,D1,(len D1)) - (indx D2,D1,j1) > 2 ; :: thesis:
set ID1 = (indx D2,D1,j1) + 1;
set ID2 = ((indx D2,D1,j1) + 1) + 1;
A74: ( indx D2,D1,j1 < (indx D2,D1,j1) + 1 & (indx D2,D1,j1) + 1 < ((indx D2,D1,j1) + 1) + 1 & ((indx D2,D1,j1) + 1) + 1 < indx D2,D1,(len D1) )

proof

thus indx D2,D1,j1 < (indx D2,D1,j1) + 1 by NAT_1:13; :: thesis:
thus (indx D2,D1,j1) + 1 < ((indx D2,D1,j1) + 1) + 1 by NAT_1:13; :: thesis:
(indx D2,D1,j1) + (1 + 1) < indx D2,D1,(len D1) by A73, XREAL_1:22;
hence ((indx D2,D1,j1) + 1) + 1 < indx D2,D1,(len D1) ; :: thesis:

end;

A75: indx D2,D1,(len D1) in dom D2 by A2, A6, INTEGRA1:def 21;
then A76: indx D2,D1,(len D1) <= len D2 by FINSEQ_3:27;
A77: (indx D2,D1,j1) + 1 in dom D2

proof

A78: ( 1 <= (indx D2,D1,j1) + 1 & (indx D2,D1,j1) + 1 <= indx D2,D1,(len D1) ) by A17, A74, XXREAL_0:2;
then (indx D2,D1,j1) + 1 <= len D2 by A76, XXREAL_0:2;
hence (indx D2,D1,j1) + 1 in dom D2 by A78, FINSEQ_3:27; :: thesis:

end;

A79: ((indx D2,D1,j1) + 1) + 1 in dom D2

proof

A80: ( indx D2,D1,j1 <= ((indx D2,D1,j1) + 1) + 1 & ((indx D2,D1,j1) + 1) + 1 <= len D2 ) by A74, A76, XXREAL_0:2;
then 1 <= ((indx D2,D1,j1) + 1) + 1 by A17, XXREAL_0:2;
hence ((indx D2,D1,j1) + 1) + 1 in dom D2 by A80, FINSEQ_3:27; :: thesis:

end;

then A81: ( D2 . (indx D2,D1,j1) < D2 . ((indx D2,D1,j1) + 1) & D2 . ((indx D2,D1,j1) + 1) < D2 . (((indx D2,D1,j1) + 1) + 1) & D2 . (((indx D2,D1,j1) + 1) + 1) < D2 . (indx D2,D1,(len D1)) ) by A17, A74, A75, A77, SEQM_3:def 1;
A82: ( D2 . ((indx D2,D1,j1) + 1) in rng D2 & D2 . (((indx D2,D1,j1) + 1) + 1) in rng D2 ) by A77, A79, FUNCT_1:def 5;
A83: ( D1 . j1 = D2 . (indx D2,D1,j1) & D1 . (len D1) = D2 . (indx D2,D1,(len D1)) ) by A2, A6, A19, INTEGRA1:def 21;
A84: ( D2 . ((indx D2,D1,j1) + 1) in {x} & D2 . (((indx D2,D1,j1) + 1) + 1) in {x} )

proof

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

proof

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

per cases by A85;

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

then consider n being Element of NAT such that
A86: ( n in dom D1 & D1 . n = D2 . ((indx D2,D1,j1) + 1) ) by PARTFUN1:26;
( D2 . (indx D2,D1,j1) < D2 . ((indx D2,D1,j1) + 1) & D2 . ((indx D2,D1,j1) + 1) < D2 . (indx D2,D1,(len D1)) ) by A81, XXREAL_0:2;
then ( j1 < n & n < len D1 ) by A6, A19, A83, A86, GOBOARD2:18;
then ( len D1 < n + 1 & n < len D1 ) by XREAL_1:21;
hence contradiction by 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
A87: ( n in dom D1 & D1 . n = D2 . (((indx D2,D1,j1) + 1) + 1) ) by PARTFUN1:26;
( D2 . (indx D2,D1,j1) < D2 . (((indx D2,D1,j1) + 1) + 1) & D2 . (((indx D2,D1,j1) + 1) + 1) < D2 . (indx D2,D1,(len D1)) ) by A81, XXREAL_0:2;
then ( j1 < n & n < len D1 ) by A6, A19, A83, A87, GOBOARD2:18;
then ( len D1 < n + 1 & n < len D1 ) by XREAL_1:21;
hence contradiction by NAT_1:13; :: thesis:

end;

hence ( D2 . ((indx D2,D1,j1) + 1) in {x} & D2 . (((indx D2,D1,j1) + 1) + 1) in {x} ) by A2, A82, XBOOLE_0:def 3; :: thesis:

end;

then D2 . ((indx D2,D1,j1) + 1) = x by TARSKI:def 1;
then D2 . ((indx D2,D1,j1) + 1) = D2 . (((indx D2,D1,j1) + 1) + 1) by A84, TARSKI:def 1;
hence contradiction by A74, A77, A79, GOBOARD2:19; :: thesis:

end;

( 1 <= ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 & ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 <= 2 )

proof

A88: (indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1) = (indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1) by A68, XREAL_1:235;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 >= 0 + 1 by XREAL_1:8;
hence ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 >= 1 ; :: thesis:
thus ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 <= 2 by A72, A88; :: thesis:

end;

then A89: ( 1 <= len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) & len (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) <= 2 ) by A68, A70, A71, JORDAN3:27;
A90: ( 1 <= len D1 & len D1 <= len (lower_volume g,D1) ) by A5, FINSEQ_1:3, INTEGRA1:def 8;
((len D1) -' (len D1)) + 1 = 1 by Lm2;
then A91: len (mid (lower_volume g,D1),(len D1),(len D1)) = 1 by A90, JORDAN3:27;
(mid (lower_volume g,D1),(len D1),(len D1)) . 1 = (lower_volume g,D1) . (len D1) by A90, JORDAN3:27;
then A92: mid (lower_volume g,D1),(len D1),(len D1) = <*((lower_volume g,D1) . (len D1))*> by A91, FINSEQ_1:57;
(indx D2,D1,j1) + 1 in Seg (len (lower_volume g,D2)) by A71, FINSEQ_1:3;
then A93: (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 8;
X: len (lower_volume g,D2) = len D2 by INTEGRA1:def 8;
(indx D2,D1,j1) + 1 in dom (lower_volume g,D2) by A71, FINSEQ_3:27;
then B93: (indx D2,D1,j1) + 1 in dom D2 by X, FINSEQ_3:31;

now

per cases by A89, Lm3;

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

A96: (indx D2,D1,j1) + 1 = indx D2,D1,(len D1)

proof

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 A68, A70, A71, JORDAN3:27;
then (indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1) = 0 by A68, A95, XREAL_1:235;
hence (indx D2,D1,j1) + 1 = indx D2,D1,(len D1) ; :: thesis:

end;

A97: divset D2,(indx D2,D1,(len D1)) = divset D1,(len D1)

proof

( lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1)) )

proof

( lower_bound (divset D1,(len D1)) = D1 . j1 & upper_bound (divset D1,(len D1)) = D1 . (len D1) ) by A6, A7, INTEGRA1:def 5;
hence ( lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1)) ) by A2, A6, A19, INTEGRA1:def 21; :: thesis:

end;

then A98: divset D1,(len D1) = [.(D2 . (indx D2,D1,j1)),(D2 . (indx D2,D1,(len D1))).] by INTEGRA1:5;
A99: indx D2,D1,(len D1) in dom D2 by A2, A6, INTEGRA1:def 21;
indx D2,D1,(len D1) <> 1 by A17, A96, NAT_1:13;
then ( lower_bound (divset D2,(indx D2,D1,(len D1))) = D2 . ((indx D2,D1,(len D1)) - 1) & upper_bound (divset D2,(indx D2,D1,(len D1))) = D2 . (indx D2,D1,(len D1)) ) by A99, INTEGRA1:def 5;
hence divset D2,(indx D2,D1,(len D1)) = divset D1,(len D1) by A96, A98, INTEGRA1:5; :: thesis:

end;

(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 A70, A71, JORDAN3:27;
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))*> by A95, FINSEQ_1:57;
then A100: 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:12
.= (lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by B93, INTEGRA1:def 8
.= (lower_volume g,D1) . (len D1) by A96, A97, A6, INTEGRA1:def 8
.= Sum (mid (lower_volume g,D1),(len D1),(len D1)) by A92, FINSOP_1:12 ;
A101: delta D1 >= 0 by Th8;
(upper_bound (rng g)) - (lower_bound (rng g)) >= 0 by A3, Lm4, XREAL_1:50;
then ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) >= 0 * (delta D1) by A101;
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 A100; :: thesis:

end;

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

A103: (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 A70, A71, JORDAN3:27;
(mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 2 = (lower_volume g,D2) . ((indx D2,D1,j1) + 2)

proof

A104: 2 + ((indx D2,D1,j1) + 1) >= 0 + 1 by XREAL_1:9;
(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 A68, A70, A71, A102, JORDAN3:27
.= H₂(D2) . ((2 + ((indx D2,D1,j1) + 1)) - 1) by A104, XREAL_1:235
.= H₂(D2) . ((indx D2,D1,j1) + (1 + 1)) ;
hence (mid (lower_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 2 = (lower_volume g,D2) . ((indx D2,D1,j1) + 2) ; :: thesis:

end;

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 A102, A103, FINSEQ_1:61;
then A105: 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:107;
A106: vol (divset D1,(len D1)) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))

proof

A107: ( lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1)) )

proof

end;

A108: indx D2,D1,(len D1) = (indx D2,D1,j1) + 2

proof

((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A68, A70, A71, A102, JORDAN3:27;
then ((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1 = 2 by A68, XREAL_1:235;
hence indx D2,D1,(len D1) = (indx D2,D1,j1) + 2 ; :: thesis:

end;

A109: ( lower_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 1) & upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2) & lower_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . ((indx D2,D1,j1) + 1) )

proof

A110: (indx D2,D1,j1) + 2 in dom D2 by A2, A6, A108, INTEGRA1:def 21;
(indx D2,D1,j1) + 1 in Seg (len (lower_volume g,D2)) by A71, FINSEQ_1:3;
then (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 8;
then A111: (indx D2,D1,j1) + 1 in dom D2 by FINSEQ_1:def 3;
A112: (indx D2,D1,j1) + 1 <> 1 by A17, NAT_1:13;
A113: ((indx D2,D1,j1) + 1) + 1 > 1 by A71, NAT_1:13;
A114: ((indx D2,D1,j1) + 2) - 1 = (indx D2,D1,j1) + 1 ;
A115: ((indx D2,D1,j1) + 1) - 1 = (indx D2,D1,j1) + 0 ;
thus ( lower_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 1) & upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2) ) by A110, A113, A114, INTEGRA1:def 5; :: thesis:
thus ( lower_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . ((indx D2,D1,j1) + 1) ) by A111, A112, A115, INTEGRA1:def 5; :: thesis:

end;

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 A107, A108, INTEGRA1:def 6;
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 A109, INTEGRA1:def 6
.= (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 A109 ;
hence vol (divset D1,(len D1)) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2))) by INTEGRA1:def 6; :: thesis:

end;

then A116: (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 A6, INTEGRA1:def 8;
A117: vol (divset D2,((indx D2,D1,j1) + 1)) >= 0 by INTEGRA1:11;
A118: vol (divset D2,((indx D2,D1,j1) + 2)) >= 0 by INTEGRA1:11;
A119: (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

A120: indx D2,D1,(len D1) in dom D2 by A2, A6, INTEGRA1:def 21;
A121: indx D2,D1,(len D1) = (indx D2,D1,j1) + 2

proof

end;

set ID1 = (indx D2,D1,j1) + 1;
set ID2 = (indx D2,D1,j1) + 2;
A123: 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 A105, A120, A121, INTEGRA1:def 8
.= ((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 B93, INTEGRA1:def 8 ;
divset D2,((indx D2,D1,j1) + 2) c= A by A120, A121, INTEGRA1:10;
then A124: lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 2)))) <= upper_bound (rng g) by A3, Lm5;
(indx D2,D1,j1) + 1 in dom D2 by A93, FINSEQ_1:def 3;
then divset D2,((indx D2,D1,j1) + 1) c= A by INTEGRA1:10;
then lower_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1)))) <= upper_bound (rng g) by A3, Lm5;
then A125: (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 A117, XREAL_1:66;
divset D1,(len D1) c= A by A6, INTEGRA1:10;
then A126: lower_bound (rng (g | (divset D1,(len D1)))) >= lower_bound (rng g) by A3, Lm5;
then A127: ( (lower_bound (rng (g | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 2))) >= (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))) >= (lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 1))) ) by A117, A118, XREAL_1:66;
(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 A118, A123, A124, XREAL_1:66;
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:22;
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:22;
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 A125, XXREAL_0:2;
then A128: 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:22;
set IR = (lower_bound (rng g)) * (vol (divset D2,((indx D2,D1,j1) + 2)));
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 A92, A116, FINSOP_1:12;
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 A118, A126, XREAL_1:66;
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:21;
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 | (divset D1,(len D1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by XREAL_1:21;
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 A127, XXREAL_0:2;
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 XREAL_1:21;
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 A128, XREAL_1:15;
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 A3, Lm4, XREAL_1:50;
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, Lm6, XREAL_1:66;
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 A106, A119, 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;

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

proof

U: indx D2,D1,(len D1) in dom D2 by A2, A6, INTEGRA1:def 21;
then indx D2,D1,(len D1) in Seg (len D2) by FINSEQ_1:def 3;
then A131: ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len D2 ) by FINSEQ_1:3;
then A132: indx D2,D1,(len D1) <= len H₂(D2) by INTEGRA1:def 8;
T: len D2 = len H₂(D2) by INTEGRA1:def 8;
then B133: indx D2,D1,(len D1) in dom H₂(D2) by U, FINSEQ_3:31;
A134: indx D2,D1,j1 < indx D2,D1,(len D1) by A68, NAT_1:13;
indx D2,D1,j1 in dom H₂(D2) by T, A17, FINSEQ_3:31;
then H₁(D2, indx D2,D1,j1) = Sum (H₂(D2) | (indx D2,D1,j1)) by INTEGRA1:def 22;
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:105
.= Sum ((mid H₂(D2),1,(indx D2,D1,j1)) ^ (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) by A17, JORDAN3:25
.= Sum (mid H₂(D2),1,(indx D2,D1,(len D1))) by A17, A132, A134, INTEGRA2:4
.= Sum (H₂(D2) | (indx D2,D1,(len D1))) by A131, JORDAN3:25 ;
hence 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 B133, INTEGRA1:def 22; :: thesis:

end;

A135: H₁(D1,j1) + (Sum (mid (lower_volume g,D1),(len D1),(len D1))) = H₁(D1, len D1)

proof

A136: ( 1 <= len D1 & len D1 <= len H₂(D1) ) by A5, FINSEQ_1:3, INTEGRA1:def 8;
then A137: len D1 in dom H₂(D1) by FINSEQ_3:27;
len D1 < (len D1) + 1 by NAT_1:13;
then A138: j1 < len D1 by XREAL_1:21;
j1 < len H₂(D1) by A138, A136, XXREAL_0:2;
then j1 in dom H₂(D1) by A19, FINSEQ_3:27;
then H₁(D1,j1) = Sum (H₂(D1) | j1) by INTEGRA1:def 22;
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:105
.= Sum ((mid H₂(D1),1,j1) ^ (mid H₂(D1),(j1 + 1),(len D1))) by A19, JORDAN3:25
.= Sum (mid H₂(D1),1,(len D1)) by A19, A136, A138, INTEGRA2:4
.= Sum (H₂(D1) | (len D1)) by A136, JORDAN3:25 ;
hence H₁(D1,j1) + (Sum (mid (lower_volume g,D1),(len D1),(len D1))) = H₁(D1, len D1) by A137, INTEGRA1:def 22; :: thesis:

end;

B14: indx D2,D1,(len D1) in dom (lower_volume g,D2) by A14, FINSEQ_1:def 3;
B15: len D1 in dom (lower_volume g,D1) by A15, FINSEQ_1:def 3;
A139: H₁(D2, indx D2,D1,(len D1)) = Sum ((lower_volume g,D2) | (indx D2,D1,(len D1))) by B14, INTEGRA1:def 22
.= Sum (lower_volume g,D2) by A10, FINSEQ_1:79 ;
H₁(D1, len D1) = Sum ((lower_volume g,D1) | (len D1)) by B15, INTEGRA1:def 22
.= Sum (lower_volume g,D1) by A15, FINSEQ_1:79 ;
hence (Sum (lower_volume g,D2)) - (Sum (lower_volume g,D1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A67, A69, A129, A135, A139; :: thesis: