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₁( Division of A) -> FinSequence of REAL = upper_volume (g,$1);
deffunc H₂( 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))

proof

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

proof

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) in rng D2 by A16, 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 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;

indx (D2,D1,(len D1)) in Seg (len D2) by A7, FINSEQ_1:def 3;
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₂(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)

proof

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

proof

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 )

proof

assume A44: ( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 ) ; :: thesis: contradiction

now :: thesis: contradiction

per cases ( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 ) by A44;

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;

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;

end;

end;

hence contradiction ; :: thesis: verum

end;

D2 . ID1 in rng D2 by A39, FUNCT_1:def 3;
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;

A52: len D1 <= len (upper_volume (g,D1)) by INTEGRA1:def 6;
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)

per 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;

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;

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₁(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1) by A15, A58, A59, A56, A60, A74, FINSEQ_6:118
.= H₁(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) - 1) by A76, XREAL_1:233
.= H₁(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₁(D1),(len D1),(len D1)))) - (Sum (mid (H₁(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)))))

proof

set ID1 = (indx (D2,D1,j1)) + 1;
set ID2 = (indx (D2,D1,j1)) + 2;
A93: (Sum (mid (H₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(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₁(D1),(len D1),(len D1)))) - (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)))))) - (((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₁(D1),(len D1),(len D1)))) - (Sum (mid (H₁(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;

(upper_bound (rng g)) - (lower_bound (rng g)) >= 0 by A27, 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 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;

end;

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

end;

len D1 in Seg (len (upper_volume (g,D1))) by A5, INTEGRA1:def 6;
then len D1 in dom (upper_volume (g,D1)) by FINSEQ_1:def 3;
then A101: H₂(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₁(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)

proof

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

now :: thesis: contradiction

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

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;

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;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

proof

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

proof

per cases ( k = 1 or k <> 1 ) ;

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;

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;

end;

end;

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

indx (D2,D1,j1) in dom D2 by A3, A10, INTEGRA1:def 19;
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₁(D2) by INTEGRA1:def 6;
then A160: indx (D2,D1,(len D1)) in dom H₁(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₁(D2)) by INTEGRA1:def 6;
then indx (D2,D1,j1) in dom H₁(D2) by FINSEQ_1:def 3;
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 ((upper_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 A12, FINSEQ_6:116
.= Sum (mid (H₁(D2),1,(indx (D2,D1,(len D1))))) by A12, A14, A159, INTEGRA2:4
.= Sum (H₁(D2) | (indx (D2,D1,(len D1)))) by A23, FINSEQ_6:116 ;
then A161: H₂(D2, indx (D2,D1,j1)) + (Sum (mid ((upper_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) = H₂(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₁(D1) by A102, FINSEQ_3:25;
j1 in Seg (len D1) by A10, FINSEQ_1:def 3;
then j1 in Seg (len H₁(D1)) by INTEGRA1:def 6;
then j1 in dom H₁(D1) by FINSEQ_1:def 3;
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 A103, FINSEQ_6:116
.= Sum (mid (H₁(D1),1,(len D1))) by A103, A102, A158, INTEGRA2:4
.= Sum (H₁(D1) | (len D1)) by A162, FINSEQ_6:116 ;
then A164: H₂(D1,j1) + (Sum (mid ((upper_volume (g,D1)),(len D1),(len D1)))) = H₂(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₂(D2, indx (D2,D1,j1)) = Sum ((upper_volume (g,D2)) | (indx (D2,D1,j1))) by INTEGRA1:def 20
.= H₂(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