let x be Real; :: thesis: for A being 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 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:5;
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 21;
deffunc H₁( Division of A) -> FinSequence of REAL = upper_volume g,$1;
deffunc H₂( Division of A, Nat) -> Element of REAL = (PartSums (upper_volume g,$1)) . $2;
A8: len D1 >= len (upper_volume g,D1) by INTEGRA1:def 7;
A9: len D1 <> 1 by A2;
then A10: (len D1) - 1 in dom D1 by A6, INTEGRA1:9;
reconsider j1 = (len D1) - 1 as Element of NAT by A6, A9, INTEGRA1:9;
A11: indx D2,D1,j1 in dom D2 by A3, A10, INTEGRA1:def 21;
then A12: 1 <= indx D2,D1,j1 by FINSEQ_3:27;
then mid D2,1,(indx D2,D1,j1) is increasing by A11, INTEGRA1:37;
then A13: D2 | (indx D2,D1,j1) is increasing by A12, JORDAN3:25;
len D1 < (len D1) + 1 by NAT_1:13;
then j1 < len D1 by XREAL_1:21;
then A14: indx D2,D1,j1 < indx D2,D1,(len D1) by A3, A6, A10, Th7;
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:5;
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 21;
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 7;
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 5;
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 5; :: 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 7;
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 22
.= Sum (upper_volume g,D2) by A18, FINSEQ_1:79 ;
indx D2,D1,(len D1) in dom D2 by A3, A6, INTEGRA1:def 21;
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:3;
A24: indx D2,D1,j1 <= len D2 by A11, FINSEQ_3:27;
then A25: len (D2 | (indx D2,D1,j1)) = indx D2,D1,j1 by FINSEQ_1:80;
A26: j1 <= len D1 by A10, FINSEQ_3:27;
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:22;
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 21;
then A34: indx D2,D1,(len D1) <= len D2 by FINSEQ_3:27;
then ID2 <= len D2 by A30, XXREAL_0:2;
then A35: ID2 in dom D2 by A32, FINSEQ_3:27;
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 21;
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:27;
A40: D1 . (len D1) = D2 . (indx D2,D1,(len D1)) by A3, A6, INTEGRA1:def 21;
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

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:26;
j1 < n by A10, A41, A38, A45, A46, GOBOARD2:18;
then A47: len D1 < n + 1 by XREAL_1:21;
D2 . ID1 < D2 . (indx D2,D1,(len D1)) by A42, A36, XXREAL_0:2;
then n < len D1 by A6, A40, A45, A46, GOBOARD2:18;
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:26;
D2 . (indx D2,D1,j1) < D2 . ID2 by A41, A42, XXREAL_0:2;
then j1 < n by A10, A38, A48, A49, GOBOARD2:18;
then A50: len D1 < n + 1 by XREAL_1:21;
n < len D1 by A6, A36, A40, A48, A49, GOBOARD2:18;
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 5;
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 5;
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, GOBOARD2:19; :: thesis: verum

end;

A52: len D1 <= len (upper_volume g,D1) by INTEGRA1:def 7;
A53: 1 <= len D1 by A5, FINSEQ_1:3;
then A54: (mid (upper_volume g,D1),(len D1),(len D1)) . 1 = (upper_volume g,D1) . (len D1) by A52, JORDAN3:27;
((len D1) -' (len D1)) + 1 = 1 by Lm1;
then len (mid (upper_volume g,D1),(len D1),(len D1)) = 1 by A53, A52, JORDAN3:27;
then mid (upper_volume g,D1),(len D1),(len D1) = <*((upper_volume g,D1) . (len D1))*> by A54, FINSEQ_1:57;
then A55: Sum (mid (upper_volume g,D1),(len D1),(len D1)) = (upper_volume g,D1) . (len D1) by FINSOP_1:12;
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 21;
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:3;
indx D2,D1,(len D1) in Seg (len (upper_volume g,D2)) by A57, INTEGRA1:def 7;
then A59: indx D2,D1,(len D1) <= len (upper_volume g,D2) by FINSEQ_1:3;
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:3;
then A61: (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7;
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:235;
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, JORDAN3:27;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 >= 0 + 1 by XREAL_1:8;
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, JORDAN3:27;

now

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 5;
then A66: upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1)) by A3, A6, INTEGRA1:def 21;
lower_bound (divset D1,(len D1)) = D1 . j1 by A6, A9, INTEGRA1:def 5;
then lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1) by A3, A10, INTEGRA1:def 21;
then A67: divset D1,(len D1) = [.(D2 . (indx D2,D1,j1)),(D2 . (indx D2,D1,(len D1))).] by A66, INTEGRA1:5;
A68: delta D1 >= 0 by Th8;
A69: (upper_bound (rng g)) - (lower_bound (rng g)) >= 0 by A27, Lm3, XREAL_1:50;
A70: indx D2,D1,(len D1) in dom D2 by A3, A6, INTEGRA1:def 21;
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, JORDAN3:27;
then A71: (indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1) = 0 by A15, A65, XREAL_1:235;
then indx D2,D1,(len D1) <> 1 by A11, FINSEQ_3:27;
then A72: upper_bound (divset D2,(indx D2,D1,(len D1))) = D2 . (indx D2,D1,(len D1)) by A70, INTEGRA1:def 5;
lower_bound (divset D2,(indx D2,D1,(len D1))) = D2 . ((indx D2,D1,(len D1)) - 1) by A12, A71, A70, INTEGRA1:def 5;
then A73: divset D2,(indx D2,D1,(len D1)) = divset D1,(len D1) by A71, A67, A72, INTEGRA1:5;
(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, JORDAN3:27;
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))*> by A65, FINSEQ_1:57;
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:12
.= (upper_bound (rng (g | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by A62, INTEGRA1:def 7
.= Sum (mid (upper_volume g,D1),(len D1),(len D1)) by A6, A55, A71, A73, INTEGRA1:def 7 ;
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, JORDAN3:27;
A76: 2 + ((indx D2,D1,j1) + 1) >= 0 + 1 by XREAL_1:9;
(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, JORDAN3:27
.= H₁(D2) . ((2 + ((indx D2,D1,j1) + 1)) - 1) by A76, XREAL_1:235
.= 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:61;
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:107;
A78: vol (divset D2,((indx D2,D1,j1) + 1)) >= 0 by INTEGRA1:11;
upper_bound (divset D1,(len D1)) = D1 . (len D1) by A6, A9, INTEGRA1:def 5;
then A79: upper_bound (divset D1,(len D1)) = D2 . (indx D2,D1,(len D1)) by A3, A6, INTEGRA1:def 21;
A80: vol (divset D2,((indx D2,D1,j1) + 2)) >= 0 by INTEGRA1:11;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A15, A58, A59, A56, A60, A74, JORDAN3:27;
then A81: ((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1 = 2 by A15, XREAL_1:235;
then A82: (indx D2,D1,j1) + 2 in dom D2 by A3, A6, INTEGRA1:def 21;
lower_bound (divset D1,(len D1)) = D1 . j1 by A6, A9, INTEGRA1:def 5;
then lower_bound (divset D1,(len D1)) = D2 . (indx D2,D1,j1) by A3, A10, INTEGRA1:def 21;
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 6;
(indx D2,D1,j1) + 1 in Seg (len (upper_volume g,D2)) by A56, A60, FINSEQ_1:3;
then (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7;
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 5;
((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 5;
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 5;
upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2) by A82, A88, INTEGRA1:def 5;
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 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 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 6;
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 7;
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:10;
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:66;
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:22;
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:22;
(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:66;
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:22;
(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:10;
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:66;
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A15, A58, A59, A56, A60, A74, JORDAN3:27;
then A98: ((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1 = 2 by A15, XREAL_1:235;
A99: indx D2,D1,(len D1) in dom D2 by A3, A6, INTEGRA1:def 21;
then divset D2,((indx D2,D1,j1) + 2) c= A by A98, INTEGRA1:10;
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 7
.= ((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 7 ;
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:66;
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:21;
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:21;
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:21;
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:15;
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: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, Lm5, XREAL_1:66;
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 7;
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 22
.= Sum (upper_volume g,D1) by A8, FINSEQ_1:79 ;
A102: len D1 <= len H₁(D1) by INTEGRA1:def 7;
A103: 1 <= j1 by A10, FINSEQ_3:27;
then mid D1,1,j1 is increasing by A6, A9, INTEGRA1:9, INTEGRA1:37;
then A104: D1 | j1 is increasing by A103, JORDAN3:25;
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, Th5;
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

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:27;
then indx D2,D1,k in dom D2 by A3, INTEGRA1:def 21;
then indx D2,D1,k in Seg (len D2) by FINSEQ_1:def 3;
then A113: 1 <= indx D2,D1,k by FINSEQ_1:3;
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:3;
indx D2,D1,k <= indx D2,D1,j1 by A3, A10, A109, A112, Th6;
then indx D2,D1,k in Seg (indx D2,D1,j1) by A113, FINSEQ_1:3;
then A116: (D2 | (indx D2,D1,j1)) . (indx D2,D1,k) = D2 . (indx D2,D1,k) by A11, RFINSEQ:19;
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:3;
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 21;
hence contradiction by A10, A106, A116, A117, A115, RFINSEQ:19; :: 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:27;
then indx D2,D1,k <= indx D2,D1,j1 by A3, A10, A109, Th6;
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:27;
k in Seg j1 by A108, A109, FINSEQ_1:3;
then A122: D1 . k = (D1 | j1) . k by A10, RFINSEQ:19;
indx D2,D1,k in dom D2 by A3, A119, INTEGRA1:def 21;
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:3;
D1 . k = D2 . (indx D2,D1,k) by A3, A119, INTEGRA1:def 21;
hence contradiction by A11, A106, A122, A123, A124, RFINSEQ:19; :: 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 7;
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 13;
A129: len (upper_volume g,D1) = len D1 by INTEGRA1:def 7;
then A130: k <= j1 by A26, A128, FINSEQ_1:80;
then A131: k <= len D1 by A26, XXREAL_0:2;
then k in Seg (len D1) by A127, FINSEQ_1:3;
then A132: k in dom D1 by FINSEQ_1:def 3;
then A133: indx D2,D1,k in dom D2 by A3, INTEGRA1:def 21;
A134: k in Seg j1 by A127, A130, FINSEQ_1:3;
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:3;
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 21;
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 5;
A141: lower_bound (divset D1,k) = lower_bound A by A132, A139, INTEGRA1:def 5;
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 5; :: 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:9;
k <= k + 1 by NAT_1:11;
then k1 <= k by XREAL_1:22;
then A143: k1 <= j1 by A130, XXREAL_0:2;
A144: k - 1 in dom D1 by A132, A142, INTEGRA1:9;
then 1 <= k1 by FINSEQ_3:27;
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 5;
A148: upper_bound (divset D2,(indx D2,D1,k)) = D2 . (indx D2,D1,k) by A133, A146, INTEGRA1:def 5;
A149: upper_bound (divset D1,k) = D1 . k by A132, A142, INTEGRA1:def 5;
lower_bound (divset D1,k) = D1 . (k - 1) by A132, A142, INTEGRA1:def 5;
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 21; :: thesis: verum

end;

end;

end;

divset D1,k = [.(lower_bound (divset D1,k)),(upper_bound (divset D1,k)).] by INTEGRA1:5;
then A150: divset D1,k = divset D2,(indx D2,D1,k) by A138, INTEGRA1:5;
A151: k in dom D1 by A127, A131, FINSEQ_3:27;
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:19
.= (upper_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by A151, A150, INTEGRA1:def 7 ;
1 <= indx D2,D1,k by A107, A127, A130;
then A153: indx D2,D1,k in dom D2 by A136, FINSEQ_3:27;
((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:19
.= (upper_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by A153, INTEGRA1:def 7 ;
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 21;
then indx D2,D1,j1 <= len D2 by FINSEQ_3:27;
then A154: indx D2,D1,j1 <= len (upper_volume g,D2) by INTEGRA1:def 7;
j1 in Seg (len D1) by A10, FINSEQ_1:def 3;
then j1 <= len D1 by FINSEQ_1:3;
then A155: j1 <= len (upper_volume g,D1) by INTEGRA1:def 7;
len (D2 | (indx D2,D1,j1)) = len (D1 | j1) by A13, A104, A105, Th5;
then indx D2,D1,j1 = j1 by A26, A25, FINSEQ_1:80;
then len ((upper_volume g,D1) | j1) = indx D2,D1,j1 by A155, FINSEQ_1:80;
then len ((upper_volume g,D1) | j1) = len ((upper_volume g,D2) | (indx D2,D1,j1)) by A154, FINSEQ_1:80;
then A156: (upper_volume g,D2) | (indx D2,D1,j1) = (upper_volume g,D1) | j1 by A125, FINSEQ_1:18;
j1 in Seg (len D1) by A10, FINSEQ_1:def 3;
then j1 in Seg (len (upper_volume g,D1)) by INTEGRA1:def 7;
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:21;
indx D2,D1,(len D1) <= len D2 by A22, FINSEQ_1:3;
then A159: indx D2,D1,(len D1) <= len H₁(D2) by INTEGRA1:def 7;
then A160: indx D2,D1,(len D1) in dom H₁(D2) by A23, FINSEQ_3:27;
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 7;
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 22;
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:105
.= Sum ((mid H₁(D2),1,(indx D2,D1,j1)) ^ (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) by A12, JORDAN3:25
.= 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, JORDAN3:25 ;
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 22;
A162: 1 <= len D1 by A5, FINSEQ_1:3;
then A163: len D1 in dom H₁(D1) by A102, FINSEQ_3:27;
j1 in Seg (len D1) by A10, FINSEQ_1:def 3;
then j1 in Seg (len H₁(D1)) by INTEGRA1:def 7;
then j1 in dom H₁(D1) by FINSEQ_1:def 3;
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 A103, JORDAN3:25
.= Sum (mid H₁(D1),1,(len D1)) by A103, A102, A158, INTEGRA2:4
.= Sum (H₁(D1) | (len D1)) by A162, JORDAN3:25 ;
then A164: H₂(D1,j1) + (Sum (mid (upper_volume g,D1),(len D1),(len D1))) = H₂(D1, len D1) by A163, INTEGRA1:def 22;
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 7;
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 22
.= H₂(D1,j1) by A156, A157, INTEGRA1:def 22 ;
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