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 A1: ( x in divset D1,(len D1) & 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) )
assume A2: ( D1 <= D2 & 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) )
assume A3: 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)
deffunc H1( Division of A, Nat) -> Element of REAL = (PartSums (upper_volume g,$1)) . $2;
deffunc H2( Division of A) -> FinSequence of REAL = upper_volume g,$1;
set j = len D1;
A4: ( len D1 in Seg (len D1) & len D2 in Seg (len D2) ) by FINSEQ_1:5;
then A5: ( len D1 in dom D1 & len D2 in dom D2 ) by FINSEQ_1:def 3;
A6: len D1 <> 1 by A1;
A7: ( indx D2,D1,(len D1) in dom D2 & D2 . (indx D2,D1,(len D1)) = D1 . (len D1) ) by A2, A5, INTEGRA1:def 21;
then A8: indx D2,D1,(len D1) in Seg (len D2) by FINSEQ_1:def 3;
A9: 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 A10: D1 . (len D1) < D2 . (len D2) by A5, A7, SEQM_3:def 1;
A11: not D2 . (len D2) in rng D1
proof
assume A12: D2 . (len D2) in rng D1 ; :: thesis: contradiction
rng D1 c= A by INTEGRA1:def 2;
then ( lower_bound A <= D2 . (len D2) & D2 . (len D2) <= upper_bound A ) by A12, INTEGRA2:1;
hence contradiction by A10, INTEGRA1:def 2; :: thesis: verum
end;
D2 . (len D2) in rng D2 by A5, 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 A11, TARSKI:def 1;
then D2 . (len D2) <= upper_bound (divset D1,(len D1)) by A1, INTEGRA2:1;
hence contradiction by A5, A6, A10, INTEGRA1:def 5; :: thesis: verum
end;
then A13: ( indx D2,D1,(len D1) in Seg (len (upper_volume g,D2)) & indx D2,D1,(len D1) >= len (upper_volume g,D2) ) by A8, INTEGRA1:def 7;
A14: ( len D1 in Seg (len (upper_volume g,D1)) & len D1 >= len (upper_volume g,D1) ) by A4, INTEGRA1:def 7;
A15: ( (len D1) - 1 in NAT & (len D1) - 1 in dom D1 ) by A5, A6, INTEGRA1:9;
reconsider j1 = (len D1) - 1 as Element of NAT by A5, A6, INTEGRA1:9;
A16: ( 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, A15, INTEGRA1:def 21; :: thesis: ( 1 <= indx D2,D1,j1 & indx D2,D1,j1 <= len D2 )
hence ( 1 <= indx D2,D1,j1 & indx D2,D1,j1 <= len D2 ) by FINSEQ_3:27; :: thesis: verum
end;
then mid D2,1,(indx D2,D1,j1) is increasing by INTEGRA1:37;
then A17: D2 | (indx D2,D1,j1) is increasing by A16, JORDAN3:25;
A18: ( j1 in dom D1 & 1 <= j1 & j1 <= len D1 ) by A15, FINSEQ_3:27;
then mid D1,1,j1 is increasing by INTEGRA1:37;
then A19: D1 | j1 is increasing by A18, JORDAN3:25;
A20: rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1) by A1, A2, Lm7;
then A21: D2 | (indx D2,D1,j1) = D1 | j1 by A17, A19, Th5;
A22: 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 A23: ( 1 <= k & k <= j1 ) ; :: thesis: k = indx D2,D1,k
assume A24: k <> indx D2,D1,k ; :: thesis: contradiction
now
per cases ( k > indx D2,D1,k or k < indx D2,D1,k ) by A24, XXREAL_0:1;
suppose A25: k > indx D2,D1,k ; :: thesis: contradiction
( 1 <= k & k <= len D1 ) by A18, A23, XXREAL_0:2;
then A26: k in dom D1 by FINSEQ_3:27;
then A27: ( 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 A28: ( 1 <= indx D2,D1,k & indx D2,D1,k <= indx D2,D1,j1 ) by A2, A15, A23, A26, Th6, FINSEQ_1:3;
then indx D2,D1,k in Seg (indx D2,D1,j1) by FINSEQ_1:3;
then A29: (D2 | (indx D2,D1,j1)) . (indx D2,D1,k) = D2 . (indx D2,D1,k) by A16, RFINSEQ:19;
A30: indx D2,D1,k < j1 by A23, A25, XXREAL_0:2;
then indx D2,D1,k <= len D1 by A18, XXREAL_0:2;
then indx D2,D1,k in Seg (len D1) by A28, FINSEQ_1:3;
then indx D2,D1,k in dom D1 by FINSEQ_1:def 3;
then A31: D1 . k > D1 . (indx D2,D1,k) by A25, A26, SEQM_3:def 1;
indx D2,D1,k in Seg j1 by A28, A30, FINSEQ_1:3;
hence contradiction by A15, A21, A27, A29, A31, RFINSEQ:19; :: thesis: verum
end;
suppose A32: k < indx D2,D1,k ; :: thesis: contradiction
k in Seg j1 by A23, FINSEQ_1:3;
then A33: D1 . k = (D1 | j1) . k by A15, RFINSEQ:19;
( 1 <= k & k <= len D1 ) by A18, A23, XXREAL_0:2;
then A34: k in dom D1 by FINSEQ_3:27;
then A35: ( 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, A15, A23, A34, Th6;
then A36: k <= indx D2,D1,j1 by A32, XXREAL_0:2;
then k <= len D2 by A16, XXREAL_0:2;
then k in dom D2 by A23, FINSEQ_3:27;
then A37: D2 . k < D2 . (indx D2,D1,k) by A32, A35, SEQM_3:def 1;
k in Seg (indx D2,D1,j1) by A23, A36, FINSEQ_1:3;
hence contradiction by A16, A21, A33, A35, A37, RFINSEQ:19; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A38: len (D2 | (indx D2,D1,j1)) = len (D1 | j1) by A17, A19, A20, Th5;
len (D2 | (indx D2,D1,j1)) = indx D2,D1,j1 by A16, FINSEQ_1:80;
then A39: indx D2,D1,j1 = j1 by A18, A38, FINSEQ_1:80;
j1 in Seg (len D1) by A15, FINSEQ_1:def 3;
then j1 <= len D1 by FINSEQ_1:3;
then j1 <= len (upper_volume g,D1) by INTEGRA1:def 7;
then A40: len ((upper_volume g,D1) | j1) = indx D2,D1,j1 by A39, FINSEQ_1:80;
indx D2,D1,j1 in dom D2 by A2, A15, INTEGRA1:def 21;
then indx D2,D1,j1 <= len D2 by FINSEQ_3:27;
then indx D2,D1,j1 <= len (upper_volume g,D2) by INTEGRA1:def 7;
then A41: len ((upper_volume g,D1) | j1) = len ((upper_volume g,D2) | (indx D2,D1,j1)) by A40, FINSEQ_1:80;
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
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 A42: ( 1 <= k & 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;
A43: len (upper_volume g,D1) = len D1 by INTEGRA1:def 7;
then A44: ( 1 <= k & k <= j1 ) by A18, A42, FINSEQ_1:80;
then A45: k in Seg j1 by FINSEQ_1:3;
X: ( 1 <= k & k <= len D1 ) by A18, A44, XXREAL_0:2;
then A46: k in Seg (len D1) by FINSEQ_1:3;
B46: k in dom D1 by X, FINSEQ_3:27;
A47: divset D1,k = divset D2,(indx D2,D1,k)
proof
A48: divset D1,k = [.(lower_bound (divset D1,k)),(upper_bound (divset D1,k)).] by INTEGRA1:5;
A49: k in dom D1 by A46, FINSEQ_1:def 3;
then A50: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A2, INTEGRA1:def 21;
( 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 A51: 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 A52: ( lower_bound (divset D1,k) = lower_bound A & upper_bound (divset D1,k) = D1 . k ) by A49, INTEGRA1:def 5;
indx D2,D1,k = 1 by A18, A22, A51;
hence ( lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) & upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) ) by A50, A52, INTEGRA1:def 5; :: thesis: verum
end;
suppose A53: 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 A54: ( lower_bound (divset D1,k) = D1 . (k - 1) & upper_bound (divset D1,k) = D1 . k ) by A49, INTEGRA1:def 5;
A55: ( k - 1 in dom D1 & D1 . (k - 1) in A & k - 1 in NAT ) by A49, A53, INTEGRA1:9;
reconsider k1 = k - 1 as Element of NAT by A49, A53, INTEGRA1:9;
k <= k + 1 by NAT_1:11;
then k1 <= k by XREAL_1:22;
then A56: k1 <= j1 by A44, XXREAL_0:2;
1 <= k1 by A55, FINSEQ_3:27;
then A57: k1 = indx D2,D1,k1 by A22, A56;
indx D2,D1,k <> 1 by A22, A44, A53;
then A58: ( 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 A50, INTEGRA1:def 5;
D2 . ((indx D2,D1,k) - 1) = D2 . (indx D2,D1,k1) by A22, A44, A57;
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, A49, A54, A55, A58, INTEGRA1:def 21; :: thesis: verum
end;
end;
end;
hence divset D1,k = divset D2,(indx D2,D1,k) by A48, INTEGRA1:5; :: thesis: verum
end;
j1 in Seg (len (upper_volume g,D1)) by A15, A43, FINSEQ_1:def 3;
then j1 in dom (upper_volume g,D1) by FINSEQ_1:def 3;
then A59: ((upper_volume g,D1) | j1) . k = (upper_volume g,D1) . k by A45, RFINSEQ:19
.= (upper_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by A47, B46, INTEGRA1:def 7 ;
indx D2,D1,k in Seg j1 by A22, A44, A45;
then A60: indx D2,D1,k in Seg (indx D2,D1,j1) by A18, A22;
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 A16, XXREAL_0:2;
B61: indx D2,D1,k in dom D2 by Y, FINSEQ_3:27;
indx D2,D1,j1 in Seg (len D2) by A16, FINSEQ_1:def 3;
then indx D2,D1,j1 in Seg (len (upper_volume g,D2)) by INTEGRA1:def 7;
then A62: indx D2,D1,j1 in dom (upper_volume g,D2) by FINSEQ_1:def 3;
((upper_volume g,D2) | (indx D2,D1,j1)) . k = ((upper_volume g,D2) | (indx D2,D1,j1)) . (indx D2,D1,k) by A22, A44
.= (upper_volume g,D2) . (indx D2,D1,k) by A60, A62, RFINSEQ:19
.= (upper_bound (rng (g | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by B61, INTEGRA1:def 7 ;
hence ((upper_volume g,D1) | j1) . k = ((upper_volume g,D2) | (indx D2,D1,j1)) . k by A59; :: thesis: verum
end;
then A63: (upper_volume g,D2) | (indx D2,D1,j1) = (upper_volume g,D1) | j1 by A41, FINSEQ_1:18;
indx D2,D1,j1 in Seg (len D2) by A16, FINSEQ_1:def 3;
then A64: indx D2,D1,j1 in Seg (len (upper_volume g,D2)) by INTEGRA1:def 7;
B64: indx D2,D1,j1 in dom (upper_volume g,D2) by A64, FINSEQ_1:def 3;
j1 in Seg (len D1) by A15, FINSEQ_1:def 3;
then j1 in Seg (len (upper_volume g,D1)) by INTEGRA1:def 7;
then B65: j1 in dom (upper_volume g,D1) by FINSEQ_1:def 3;
A66: H1(D2, indx D2,D1,j1) = Sum ((upper_volume g,D2) | (indx D2,D1,j1)) by B64, INTEGRA1:def 22
.= H1(D1,j1) by A63, B65, INTEGRA1:def 22 ;
A67: (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, A5, A15, Th7;
hence (indx D2,D1,j1) + 1 <= indx D2,D1,(len D1) by NAT_1:13; :: thesis: verum
end;
A68: (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
A69: ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len (upper_volume g,D2) )
proof
indx D2,D1,(len D1) in dom D2 by A2, A5, 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 (upper_volume g,D2)) by INTEGRA1:def 7;
hence ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len (upper_volume g,D2) ) by FINSEQ_1:3; :: thesis: verum
end;
then A70: ( 1 <= (indx D2,D1,j1) + 1 & (indx D2,D1,j1) + 1 <= len (upper_volume g,D2) ) by A16, A67, NAT_1:13, XXREAL_0:2;
A71: (indx D2,D1,(len D1)) - (indx D2,D1,j1) <= 2
proof
assume A72: (indx D2,D1,(len D1)) - (indx D2,D1,j1) > 2 ; :: thesis: contradiction
reconsider ID1 = (indx D2,D1,j1) + 1 as Element of NAT ;
reconsider ID2 = ID1 + 1 as Element of NAT ;
A73: ( indx D2,D1,j1 < ID1 & ID1 < ID2 & ID2 < indx D2,D1,(len D1) )
proof
thus indx D2,D1,j1 < ID1 by NAT_1:13; :: thesis: ( ID1 < ID2 & ID2 < indx D2,D1,(len D1) )
thus ID1 < ID2 by NAT_1:13; :: thesis: ID2 < indx D2,D1,(len D1)
(indx D2,D1,j1) + (1 + 1) < indx D2,D1,(len D1) by A72, XREAL_1:22;
hence ID2 < indx D2,D1,(len D1) ; :: thesis: verum
end;
A74: indx D2,D1,(len D1) in dom D2 by A2, A5, INTEGRA1:def 21;
then A75: indx D2,D1,(len D1) <= len D2 by FINSEQ_3:27;
A76: ID1 in dom D2
proof
A77: ( 1 <= ID1 & ID1 <= indx D2,D1,(len D1) ) by A16, A73, XXREAL_0:2;
then ID1 <= len D2 by A75, XXREAL_0:2;
hence ID1 in dom D2 by A77, FINSEQ_3:27; :: thesis: verum
end;
A78: ID2 in dom D2
proof
A79: ( indx D2,D1,j1 <= ID2 & ID2 <= len D2 ) by A73, A75, XXREAL_0:2;
then 1 <= ID2 by A16, XXREAL_0:2;
hence ID2 in dom D2 by A79, FINSEQ_3:27; :: thesis: verum
end;
then A80: ( D2 . (indx D2,D1,j1) < D2 . ID1 & D2 . ID1 < D2 . ID2 & D2 . ID2 < D2 . (indx D2,D1,(len D1)) ) by A16, A73, A74, A76, SEQM_3:def 1;
A81: ( D2 . ID1 in {x} & D2 . ID2 in {x} )
proof
A82: ( D2 . ID1 in rng D2 & D2 . ID2 in rng D2 ) by A76, A78, FUNCT_1:def 5;
A83: ( D1 . j1 = D2 . (indx D2,D1,j1) & D1 . (len D1) = D2 . (indx D2,D1,(len D1)) ) by A2, A5, A15, INTEGRA1:def 21;
( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )
proof
assume A84: ( 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 A84;
suppose D2 . ID1 in rng D1 ; :: thesis: contradiction
then consider n being Element of NAT such that
A85: ( n in dom D1 & D1 . n = D2 . ID1 ) by PARTFUN1:26;
( D2 . (indx D2,D1,j1) < D2 . ID1 & D2 . ID1 < D2 . (indx D2,D1,(len D1)) ) by A80, XXREAL_0:2;
then ( j1 < n & n < len D1 ) by A5, A15, A83, A85, GOBOARD2:18;
then ( len D1 < n + 1 & n < len D1 ) by XREAL_1:21;
hence contradiction by NAT_1:13; :: thesis: verum
end;
suppose D2 . ID2 in rng D1 ; :: thesis: contradiction
then consider n being Element of NAT such that
A86: ( n in dom D1 & D1 . n = D2 . ID2 ) by PARTFUN1:26;
( D2 . (indx D2,D1,j1) < D2 . ID2 & D2 . ID2 < D2 . (indx D2,D1,(len D1)) ) by A80, XXREAL_0:2;
then ( j1 < n & n < len D1 ) by A5, A15, A83, A86, GOBOARD2:18;
then ( len D1 < n + 1 & n < len D1 ) by XREAL_1:21;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence ( D2 . ID1 in {x} & D2 . ID2 in {x} ) by A2, A82, XBOOLE_0:def 3; :: thesis: verum
end;
then D2 . ID1 = x by TARSKI:def 1;
then D2 . ID1 = D2 . ID2 by A81, TARSKI:def 1;
hence contradiction by A73, A76, A78, GOBOARD2:19; :: thesis: verum
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
A87: (indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1) = (indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1) by A67, 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: ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 <= 2
thus ((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 <= 2 by A71, A87; :: thesis: verum
end;
then A88: ( 1 <= len (mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) & len (mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) <= 2 ) by A67, A69, A70, JORDAN3:27;
A89: ( 1 <= len D1 & len D1 <= len (upper_volume g,D1) ) by A4, FINSEQ_1:3, INTEGRA1:def 7;
((len D1) -' (len D1)) + 1 = 1 by Lm2;
then A90: len (mid (upper_volume g,D1),(len D1),(len D1)) = 1 by A89, JORDAN3:27;
(mid (upper_volume g,D1),(len D1),(len D1)) . 1 = (upper_volume g,D1) . (len D1) by A89, JORDAN3:27;
then mid (upper_volume g,D1),(len D1),(len D1) = <*((upper_volume g,D1) . (len D1))*> by A90, FINSEQ_1:57;
then A91: Sum (mid (upper_volume g,D1),(len D1),(len D1)) = (upper_volume g,D1) . (len D1) by FINSOP_1:12;
A92: (indx D2,D1,j1) + 1 in Seg (len D2)
proof
(indx D2,D1,j1) + 1 in Seg (len (upper_volume g,D2)) by A70, FINSEQ_1:3;
hence (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7; :: thesis: verum
end;
B92: (indx D2,D1,j1) + 1 in dom D2 by A92, FINSEQ_1:def 3;
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 A88, Lm3;
suppose A93: 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)
A94: (indx D2,D1,j1) + 1 = indx D2,D1,(len D1)
proof
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 A67, A69, A70, JORDAN3:27;
then (indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1) = 0 by A67, A93, XREAL_1:235;
hence (indx D2,D1,j1) + 1 = indx D2,D1,(len D1) ; :: thesis: verum
end;
A95: divset D2,(indx D2,D1,(len D1)) = divset D1,(len D1)
proof
( lower_bound (divset D1,(len D1)) = D1 . j1 & upper_bound (divset D1,(len D1)) = D1 . (len D1) ) by A5, A6, INTEGRA1:def 5;
then ( 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, A5, A15, INTEGRA1:def 21;
then A96: divset D1,(len D1) = [.(D2 . (indx D2,D1,j1)),(D2 . (indx D2,D1,(len D1))).] by INTEGRA1:5;
A97: indx D2,D1,(len D1) in dom D2 by A2, A5, INTEGRA1:def 21;
indx D2,D1,(len D1) <> 1 by A16, A94, 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 A97, INTEGRA1:def 5;
hence divset D2,(indx D2,D1,(len D1)) = divset D1,(len D1) by A94, A96, INTEGRA1:5; :: thesis: verum
end;
(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 A69, A70, 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 A93, FINSEQ_1:57;
then A98: 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 B92, INTEGRA1:def 7
.= Sum (mid (upper_volume g,D1),(len D1),(len D1)) by A91, A94, A95, A5, INTEGRA1:def 7 ;
A99: 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 A99;
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 A98; :: thesis: verum
end;
suppose A100: 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)
A101: (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 A69, A70, JORDAN3:27;
(mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 2 = (upper_volume g,D2) . ((indx D2,D1,j1) + 2)
proof
A102: 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 = H2(D2) . ((2 + ((indx D2,D1,j1) + 1)) -' 1) by A67, A69, A70, A100, JORDAN3:27
.= H2(D2) . ((2 + ((indx D2,D1,j1) + 1)) - 1) by A102, XREAL_1:235
.= H2(D2) . ((indx D2,D1,j1) + (1 + 1)) ;
hence (mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1))) . 2 = (upper_volume g,D2) . ((indx D2,D1,j1) + 2) ; :: thesis: verum
end;
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 A100, A101, FINSEQ_1:61;
then A103: 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;
A104: vol (divset D1,(len D1)) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))
proof
A105: ( 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 A5, A6, 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, A5, A15, INTEGRA1:def 21; :: thesis: verum
end;
A106: indx D2,D1,(len D1) = (indx D2,D1,j1) + 2
proof
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A67, A69, A70, A100, JORDAN3:27;
then ((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1 = 2 by A67, XREAL_1:235;
hence indx D2,D1,(len D1) = (indx D2,D1,j1) + 2 ; :: thesis: verum
end;
A107: ( 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
A108: (indx D2,D1,j1) + 2 in dom D2 by A2, A5, A106, INTEGRA1:def 21;
(indx D2,D1,j1) + 1 in Seg (len (upper_volume g,D2)) by A70, FINSEQ_1:3;
then (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7;
then A109: (indx D2,D1,j1) + 1 in dom D2 by FINSEQ_1:def 3;
A110: (indx D2,D1,j1) + 1 <> 1 by A16, NAT_1:13;
A111: ((indx D2,D1,j1) + 1) + 1 > 1 by A70, NAT_1:13;
A112: ((indx D2,D1,j1) + 2) - 1 = (indx D2,D1,j1) + 1 ;
A113: ((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 A108, A111, A112, INTEGRA1:def 5; :: thesis: ( 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) )
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 A109, A110, A113, INTEGRA1:def 5; :: thesis: verum
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 A105, A106, 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 A107, 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 A107 ;
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: verum
end;
then A114: (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 A5, INTEGRA1:def 7;
A115: vol (divset D2,((indx D2,D1,j1) + 1)) >= 0 by INTEGRA1:11;
A116: vol (divset D2,((indx D2,D1,j1) + 2)) >= 0 by INTEGRA1:11;
A117: (Sum (mid H2(D1),(len D1),(len D1))) - (Sum (mid H2(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
A118: indx D2,D1,(len D1) in dom D2 by A2, A5, INTEGRA1:def 21;
A120: indx D2,D1,(len D1) = (indx D2,D1,j1) + 2
proof
((indx D2,D1,(len D1)) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A67, A69, A70, A100, JORDAN3:27;
then ((indx D2,D1,(len D1)) - ((indx D2,D1,j1) + 1)) + 1 = 2 by A67, XREAL_1:235;
hence indx D2,D1,(len D1) = (indx D2,D1,j1) + 2 ; :: thesis: verum
end;
set ID1 = (indx D2,D1,j1) + 1;
set ID2 = (indx D2,D1,j1) + 2;
A121: Sum (mid H2(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)))) + (H2(D2) . ((indx D2,D1,j1) + 1)) by A103, A120, A118, 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 B92, INTEGRA1:def 7 ;
divset D2,((indx D2,D1,j1) + 2) c= A by A118, A120, INTEGRA1:10;
then A122: upper_bound (rng (g | (divset D2,((indx D2,D1,j1) + 2)))) >= lower_bound (rng g) by A3, Lm5;
(indx D2,D1,j1) + 1 in dom D2 by A92, 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 A3, Lm5;
then A123: (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 A115, XREAL_1:66;
divset D1,(len D1) c= A by A5, INTEGRA1:10;
then upper_bound (rng (g | (divset D1,(len D1)))) <= upper_bound (rng g) by A3, Lm5;
then A124: ( (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))) & (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 A115, A116, XREAL_1:66;
(Sum (mid H2(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 A116, A121, A122, XREAL_1:66;
then Sum (mid H2(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 H2(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 H2(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 A123, XXREAL_0:2;
then A125: Sum (mid H2(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;
(Sum (mid H2(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 A91, A114;
then Sum (mid H2(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 A124, XREAL_1:22;
then (Sum (mid H2(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;
then (Sum (mid H2(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 A124, XXREAL_0:2;
then Sum (mid H2(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;
then (Sum (mid H2(D1),(len D1),(len D1))) - (Sum (mid H2(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 A125, XREAL_1:15;
hence (Sum (mid H2(D1),(len D1),(len D1))) - (Sum (mid H2(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 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 A5, Lm6, 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 A104, A117, 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;
A126: H1(D2, indx D2,D1,j1) + (Sum (mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) = H1(D2, indx D2,D1,(len D1))
proof
indx D2,D1,(len D1) in dom D2 by A2, A5, INTEGRA1:def 21;
then indx D2,D1,(len D1) in Seg (len D2) by FINSEQ_1:def 3;
then A128: ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len D2 ) by FINSEQ_1:3;
then A129: ( 1 <= indx D2,D1,(len D1) & indx D2,D1,(len D1) <= len H2(D2) ) by INTEGRA1:def 7;
B130: indx D2,D1,(len D1) in dom H2(D2) by A129, FINSEQ_3:27;
A131: indx D2,D1,j1 < indx D2,D1,(len D1) by A67, NAT_1:13;
indx D2,D1,j1 in Seg (len D2) by A16, FINSEQ_1:def 3;
then indx D2,D1,j1 in Seg (len H2(D2)) by INTEGRA1:def 7;
then indx D2,D1,j1 in dom H2(D2) by FINSEQ_1:def 3;
then H1(D2, indx D2,D1,j1) = Sum (H2(D2) | (indx D2,D1,j1)) by INTEGRA1:def 22;
then H1(D2, indx D2,D1,j1) + (Sum (mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) = Sum ((H2(D2) | (indx D2,D1,j1)) ^ (mid H2(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) by RVSUM_1:105
.= Sum ((mid H2(D2),1,(indx D2,D1,j1)) ^ (mid H2(D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) by A16, JORDAN3:25
.= Sum (mid H2(D2),1,(indx D2,D1,(len D1))) by A16, A129, A131, INTEGRA2:4
.= Sum (H2(D2) | (indx D2,D1,(len D1))) by A128, JORDAN3:25 ;
hence H1(D2, indx D2,D1,j1) + (Sum (mid (upper_volume g,D2),((indx D2,D1,j1) + 1),(indx D2,D1,(len D1)))) = H1(D2, indx D2,D1,(len D1)) by B130, INTEGRA1:def 22; :: thesis: verum
end;
A132: H1(D1,j1) + (Sum (mid (upper_volume g,D1),(len D1),(len D1))) = H1(D1, len D1)
proof
A133: ( 1 <= len D1 & len D1 <= len H2(D1) ) by A4, FINSEQ_1:3, INTEGRA1:def 7;
B134: len D1 in dom H2(D1) by A133, FINSEQ_3:27;
len D1 < (len D1) + 1 by NAT_1:13;
then A135: j1 < len D1 by XREAL_1:21;
j1 in Seg (len D1) by A15, FINSEQ_1:def 3;
then j1 in Seg (len H2(D1)) by INTEGRA1:def 7;
then j1 in dom H2(D1) by FINSEQ_1:def 3;
then H1(D1,j1) = Sum (H2(D1) | j1) by INTEGRA1:def 22;
then H1(D1,j1) + (Sum (mid H2(D1),(len D1),(len D1))) = Sum ((H2(D1) | j1) ^ (mid H2(D1),(len D1),(len D1))) by RVSUM_1:105
.= Sum ((mid H2(D1),1,j1) ^ (mid H2(D1),(j1 + 1),(len D1))) by A18, JORDAN3:25
.= Sum (mid H2(D1),1,(len D1)) by A18, A133, A135, INTEGRA2:4
.= Sum (H2(D1) | (len D1)) by A133, JORDAN3:25 ;
hence H1(D1,j1) + (Sum (mid (upper_volume g,D1),(len D1),(len D1))) = H1(D1, len D1) by B134, INTEGRA1:def 22; :: thesis: verum
end;
B13: indx D2,D1,(len D1) in dom (upper_volume g,D2) by A13, FINSEQ_1:def 3;
B14: len D1 in dom (upper_volume g,D1) by A14, FINSEQ_1:def 3;
A136: H1(D2, indx D2,D1,(len D1)) = Sum ((upper_volume g,D2) | (indx D2,D1,(len D1))) by B13, INTEGRA1:def 22
.= Sum (upper_volume g,D2) by A9, FINSEQ_1:79 ;
H1(D1, len D1) = Sum ((upper_volume g,D1) | (len D1)) by B14, INTEGRA1:def 22
.= Sum (upper_volume g,D1) by A14, FINSEQ_1:79 ;
hence (Sum (upper_volume g,D1)) - (Sum (upper_volume g,D2)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) by A66, A68, A126, A132, A136; :: thesis: verum