let x be Real; 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 (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
let A be 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 (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
let D1, D2 be 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 (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
let g be Function of A,REAL; ( x in divset (D1,(len D1)) & len D1 >= 2 & D1 <= D2 & rng D2 = (rng D1) \/ {x} & g | A is bounded implies (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )
assume that
A1:
x in divset (D1,(len D1))
and
A2:
len D1 >= 2
; ( not D1 <= D2 or not rng D2 = (rng D1) \/ {x} or not g | A is bounded or (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((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}
; ( not g | A is bounded or (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1) )
A5:
len D1 in dom D1
by FINSEQ_5:6;
then A6:
indx (D2,D1,(len D1)) in dom D2
by A3, INTEGRA1:def 19;
A7:
len D1 <> 1
by A2;
then reconsider j1 = (len D1) - 1 as Element of NAT by A5, INTEGRA1:7;
A8:
j1 in dom D1
by A5, A7, INTEGRA1:7;
then A9:
j1 <= len D1
by FINSEQ_3:25;
A10:
1 <= j1
by A8, FINSEQ_3:25;
then
mid (D1,1,j1) is increasing
by A5, A7, INTEGRA1:7, INTEGRA1:35;
then A11:
D1 | j1 is increasing
by A10, FINSEQ_6:116;
A12:
(len D1) - 1 in dom D1
by A5, A7, INTEGRA1:7;
then A13:
indx (D2,D1,j1) in dom D2
by A3, INTEGRA1:def 19;
then A14:
1 <= indx (D2,D1,j1)
by FINSEQ_3:25;
then
mid (D2,1,(indx (D2,D1,j1))) is increasing
by A13, INTEGRA1:35;
then A15:
D2 | (indx (D2,D1,j1)) is increasing
by A14, FINSEQ_6:116;
A16:
indx (D2,D1,j1) <= len D2
by A13, FINSEQ_3:25;
then A17:
len (D2 | (indx (D2,D1,j1))) = indx (D2,D1,j1)
by FINSEQ_1:59;
A18:
rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1)
by A1, A2, A3, A4, Lm6;
then A19:
D2 | (indx (D2,D1,j1)) = D1 | j1
by A15, A11, Th6;
A20:
for k being Element of NAT st 1 <= k & k <= j1 holds
k = indx (D2,D1,k)
proof
let k be
Element of
NAT ;
( 1 <= k & k <= j1 implies k = indx (D2,D1,k) )
assume that A21:
1
<= k
and A22:
k <= j1
;
k = indx (D2,D1,k)
assume A23:
k <> indx (
D2,
D1,
k)
;
contradiction
per cases
( k > indx (D2,D1,k) or k < indx (D2,D1,k) )
by A23, XXREAL_0:1;
suppose A24:
k > indx (
D2,
D1,
k)
;
contradiction
k <= len D1
by A9, A22, XXREAL_0:2;
then A25:
k in dom D1
by A21, FINSEQ_3:25;
then
indx (
D2,
D1,
k)
in dom D2
by A3, INTEGRA1:def 19;
then
indx (
D2,
D1,
k)
in Seg (len D2)
by FINSEQ_1:def 3;
then A26:
1
<= indx (
D2,
D1,
k)
by FINSEQ_1:1;
A27:
indx (
D2,
D1,
k)
< j1
by A22, A24, XXREAL_0:2;
then A28:
indx (
D2,
D1,
k)
in Seg j1
by A26, FINSEQ_1:1;
indx (
D2,
D1,
k)
<= indx (
D2,
D1,
j1)
by A3, A8, A22, A25, Th7;
then
indx (
D2,
D1,
k)
in Seg (indx (D2,D1,j1))
by A26, FINSEQ_1:1;
then A29:
(D2 | (indx (D2,D1,j1))) . (indx (D2,D1,k)) = D2 . (indx (D2,D1,k))
by A13, RFINSEQ:6;
indx (
D2,
D1,
k)
<= len D1
by A9, A27, XXREAL_0:2;
then
indx (
D2,
D1,
k)
in dom D1
by A26, FINSEQ_3:25;
then A30:
D1 . k > D1 . (indx (D2,D1,k))
by A24, A25, SEQM_3:def 1;
D1 . k = D2 . (indx (D2,D1,k))
by A3, A25, INTEGRA1:def 19;
hence
contradiction
by A8, A19, A29, A30, A28, RFINSEQ:6;
verum end; suppose A31:
k < indx (
D2,
D1,
k)
;
contradiction
k <= len D1
by A9, A22, XXREAL_0:2;
then A32:
k in dom D1
by A21, FINSEQ_3:25;
then
indx (
D2,
D1,
k)
<= indx (
D2,
D1,
j1)
by A3, A8, A22, Th7;
then A33:
k <= indx (
D2,
D1,
j1)
by A31, XXREAL_0:2;
then
k <= len D2
by A16, XXREAL_0:2;
then A34:
k in dom D2
by A21, FINSEQ_3:25;
k in Seg j1
by A21, A22, FINSEQ_1:1;
then A35:
D1 . k = (D1 | j1) . k
by A12, RFINSEQ:6;
indx (
D2,
D1,
k)
in dom D2
by A3, A32, INTEGRA1:def 19;
then A36:
D2 . k < D2 . (indx (D2,D1,k))
by A31, A34, SEQM_3:def 1;
A37:
k in Seg (indx (D2,D1,j1))
by A21, A33, FINSEQ_1:1;
D1 . k = D2 . (indx (D2,D1,k))
by A3, A32, INTEGRA1:def 19;
hence
contradiction
by A13, A19, A35, A36, A37, RFINSEQ:6;
verum end; end;
end;
A38:
for k being Nat st 1 <= k & k <= len ((lower_volume (g,D1)) | j1) holds
((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k
proof
indx (
D2,
D1,
j1)
in Seg (len D2)
by A13, FINSEQ_1:def 3;
then
indx (
D2,
D1,
j1)
in Seg (len (lower_volume (g,D2)))
by INTEGRA1:def 7;
then A39:
indx (
D2,
D1,
j1)
in dom (lower_volume (g,D2))
by FINSEQ_1:def 3;
let k be
Nat;
( 1 <= k & k <= len ((lower_volume (g,D1)) | j1) implies ((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k )
assume that A40:
1
<= k
and A41:
k <= len ((lower_volume (g,D1)) | j1)
;
((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
A42:
len (lower_volume (g,D1)) = len D1
by INTEGRA1:def 7;
then A43:
k <= j1
by A9, A41, FINSEQ_1:59;
then
k <= len D1
by A9, XXREAL_0:2;
then
k in Seg (len D1)
by A40, FINSEQ_1:1;
then A44:
k in dom D1
by FINSEQ_1:def 3;
then A45:
indx (
D2,
D1,
k)
in dom D2
by A3, INTEGRA1:def 19;
A46:
k in Seg j1
by A40, A43, FINSEQ_1:1;
then
indx (
D2,
D1,
k)
in Seg j1
by A20, A40, A43;
then A47:
indx (
D2,
D1,
k)
in Seg (indx (D2,D1,j1))
by A10, A20;
then
indx (
D2,
D1,
k)
<= indx (
D2,
D1,
j1)
by FINSEQ_1:1;
then A48:
indx (
D2,
D1,
k)
<= len D2
by A16, XXREAL_0:2;
A49:
D1 . k = D2 . (indx (D2,D1,k))
by A3, A44, INTEGRA1:def 19;
A50:
(
lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) &
upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )
proof
per cases
( k = 1 or k <> 1 )
;
suppose A51:
k = 1
;
( 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:
upper_bound (divset (D1,k)) = D1 . k
by A44, INTEGRA1:def 4;
A53:
lower_bound (divset (D1,k)) = lower_bound A
by A44, A51, INTEGRA1:def 4;
indx (
D2,
D1,
k)
= 1
by A10, A20, A51;
hence
(
lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) &
upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )
by A45, A49, A53, A52, INTEGRA1:def 4;
verum end; suppose A54:
k <> 1
;
( 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 A44, INTEGRA1:7;
A55:
k - 1
in dom D1
by A44, A54, INTEGRA1:7;
then A56:
1
<= k1
by FINSEQ_3:25;
k <= k + 1
by NAT_1:11;
then
k1 <= k
by XREAL_1:20;
then A57:
k1 <= j1
by A43, XXREAL_0:2;
A58:
indx (
D2,
D1,
k)
<> 1
by A20, A40, A43, A54;
then A59:
lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1)
by A45, INTEGRA1:def 4;
A60:
upper_bound (divset (D1,k)) = D1 . k
by A44, A54, INTEGRA1:def 4;
A61:
lower_bound (divset (D1,k)) = D1 . (k - 1)
by A44, A54, INTEGRA1:def 4;
A62:
upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k))
by A45, A58, INTEGRA1:def 4;
D2 . ((indx (D2,D1,k)) - 1) =
D2 . (k - 1)
by A20, A40, A43
.=
D2 . (indx (D2,D1,k1))
by A20, A57, A56
;
hence
(
lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) &
upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )
by A3, A44, A61, A60, A55, A59, A62, INTEGRA1:def 19;
verum end; end;
end;
divset (
D1,
k)
= [.(lower_bound (divset (D1,k))),(upper_bound (divset (D1,k))).]
by INTEGRA1:4;
then A63:
divset (
D1,
k)
= divset (
D2,
(indx (D2,D1,k)))
by A50, INTEGRA1:4;
j1 in Seg (len (lower_volume (g,D1)))
by A8, A42, FINSEQ_1:def 3;
then
j1 in dom (lower_volume (g,D1))
by FINSEQ_1:def 3;
then A64:
((lower_volume (g,D1)) | j1) . k =
(lower_volume (g,D1)) . k
by A46, RFINSEQ:6
.=
(lower_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k)))))
by A44, A63, INTEGRA1:def 7
;
1
<= indx (
D2,
D1,
k)
by A20, A40, A43;
then A65:
indx (
D2,
D1,
k)
in dom D2
by A48, FINSEQ_3:25;
((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k =
((lower_volume (g,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k))
by A20, A40, A43
.=
(lower_volume (g,D2)) . (indx (D2,D1,k))
by A47, A39, RFINSEQ:6
.=
(lower_bound (rng (g | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k)))))
by A65, INTEGRA1:def 7
;
hence
((lower_volume (g,D1)) | j1) . k = ((lower_volume (g,D2)) | (indx (D2,D1,j1))) . k
by A64;
verum
end;
A66:
len D2 in dom D2
by FINSEQ_5:6;
deffunc H1( Division of A) -> FinSequence of REAL = lower_volume (g,$1);
deffunc H2( Division of A, Nat) -> set = (PartSums (lower_volume (g,$1))) . $2;
A67:
len D1 >= len (lower_volume (g,D1))
by INTEGRA1:def 7;
A68:
len D1 <= len H1(D1)
by INTEGRA1:def 7;
A69:
len D1 in Seg (len D1)
by FINSEQ_1:3;
then A70:
1 <= len D1
by FINSEQ_1:1;
then A71:
len D1 in dom H1(D1)
by A68, FINSEQ_3:25;
assume A72:
g | A is bounded
; (Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
len D1 < (len D1) + 1
by NAT_1:13;
then A73:
j1 < len D1
by XREAL_1:19;
then
j1 < len H1(D1)
by INTEGRA1:def 7;
then
j1 in dom H1(D1)
by A10, FINSEQ_3:25;
then
H2(D1,j1) = Sum (H1(D1) | j1)
by INTEGRA1:def 20;
then H2(D1,j1) + (Sum (mid (H1(D1),(len D1),(len D1)))) =
Sum ((H1(D1) | j1) ^ (mid (H1(D1),(len D1),(len D1))))
by RVSUM_1:75
.=
Sum ((mid (H1(D1),1,j1)) ^ (mid (H1(D1),(j1 + 1),(len D1))))
by A10, FINSEQ_6:116
.=
Sum (mid (H1(D1),1,(len D1)))
by A10, A68, A73, INTEGRA2:4
.=
Sum (H1(D1) | (len D1))
by A70, FINSEQ_6:116
;
then A74:
H2(D1,j1) + (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) = H2(D1, len D1)
by A71, INTEGRA1:def 20;
A75:
indx (D2,D1,(len D1)) in dom D2
by A3, A5, INTEGRA1:def 19;
then A76:
indx (D2,D1,(len D1)) in Seg (len D2)
by FINSEQ_1:def 3;
then A77:
1 <= indx (D2,D1,(len D1))
by FINSEQ_1:1;
len D1 < (len D1) + 1
by NAT_1:13;
then
j1 < len D1
by XREAL_1:19;
then A78:
indx (D2,D1,j1) < indx (D2,D1,(len D1))
by A3, A5, A8, Th8;
then A79:
(indx (D2,D1,j1)) + 1 <= indx (D2,D1,(len D1))
by NAT_1:13;
A80:
j1 in dom D1
by A5, A7, INTEGRA1:7;
A81:
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
proof
A82:
(indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) <= 2
proof
set ID1 =
(indx (D2,D1,j1)) + 1;
set ID2 =
((indx (D2,D1,j1)) + 1) + 1;
assume
(indx (D2,D1,(len D1))) - (indx (D2,D1,j1)) > 2
;
contradiction
then A83:
(indx (D2,D1,j1)) + (1 + 1) < indx (
D2,
D1,
(len D1))
by XREAL_1:20;
A84:
(indx (D2,D1,j1)) + 1
< ((indx (D2,D1,j1)) + 1) + 1
by NAT_1:13;
then
indx (
D2,
D1,
j1)
<= ((indx (D2,D1,j1)) + 1) + 1
by NAT_1:13;
then A85:
1
<= ((indx (D2,D1,j1)) + 1) + 1
by A14, XXREAL_0:2;
A86:
indx (
D2,
D1,
(len D1))
in dom D2
by A3, A5, INTEGRA1:def 19;
then A87:
indx (
D2,
D1,
(len D1))
<= len D2
by FINSEQ_3:25;
then
((indx (D2,D1,j1)) + 1) + 1
<= len D2
by A83, XXREAL_0:2;
then A88:
((indx (D2,D1,j1)) + 1) + 1
in dom D2
by A85, FINSEQ_3:25;
then A89:
D2 . (((indx (D2,D1,j1)) + 1) + 1) < D2 . (indx (D2,D1,(len D1)))
by A83, A86, SEQM_3:def 1;
A90:
1
<= (indx (D2,D1,j1)) + 1
by A14, NAT_1:13;
A91:
D1 . j1 = D2 . (indx (D2,D1,j1))
by A3, A8, INTEGRA1:def 19;
(indx (D2,D1,j1)) + 1
<= indx (
D2,
D1,
(len D1))
by A83, A84, XXREAL_0:2;
then
(indx (D2,D1,j1)) + 1
<= len D2
by A87, XXREAL_0:2;
then A92:
(indx (D2,D1,j1)) + 1
in dom D2
by A90, FINSEQ_3:25;
A93:
D1 . (len D1) = D2 . (indx (D2,D1,(len D1)))
by A3, A5, INTEGRA1:def 19;
indx (
D2,
D1,
j1)
< (indx (D2,D1,j1)) + 1
by NAT_1:13;
then A94:
D2 . (indx (D2,D1,j1)) < D2 . ((indx (D2,D1,j1)) + 1)
by A13, A92, SEQM_3:def 1;
A95:
D2 . ((indx (D2,D1,j1)) + 1) < D2 . (((indx (D2,D1,j1)) + 1) + 1)
by A84, A92, A88, SEQM_3:def 1;
A96:
( not
D2 . ((indx (D2,D1,j1)) + 1) in rng D1 & not
D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )
proof
assume A97:
(
D2 . ((indx (D2,D1,j1)) + 1) in rng D1 or
D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )
;
contradiction
per cases
( D2 . ((indx (D2,D1,j1)) + 1) in rng D1 or D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1 )
by A97;
suppose
D2 . ((indx (D2,D1,j1)) + 1) in rng D1
;
contradictionthen consider n being
Element of
NAT such that A98:
n in dom D1
and A99:
D1 . n = D2 . ((indx (D2,D1,j1)) + 1)
by PARTFUN1:3;
j1 < n
by A80, A94, A91, A98, A99, SEQ_4:137;
then A100:
len D1 < n + 1
by XREAL_1:19;
D2 . ((indx (D2,D1,j1)) + 1) < D2 . (indx (D2,D1,(len D1)))
by A95, A89, XXREAL_0:2;
then
n < len D1
by A5, A93, A98, A99, SEQ_4:137;
hence
contradiction
by A100, NAT_1:13;
verum end; suppose
D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D1
;
contradictionthen consider n being
Element of
NAT such that A101:
n in dom D1
and A102:
D1 . n = D2 . (((indx (D2,D1,j1)) + 1) + 1)
by PARTFUN1:3;
D2 . (indx (D2,D1,j1)) < D2 . (((indx (D2,D1,j1)) + 1) + 1)
by A94, A95, XXREAL_0:2;
then
j1 < n
by A8, A91, A101, A102, SEQ_4:137;
then A103:
len D1 < n + 1
by XREAL_1:19;
n < len D1
by A5, A89, A93, A101, A102, SEQ_4:137;
hence
contradiction
by A103, NAT_1:13;
verum end; end;
end;
D2 . ((indx (D2,D1,j1)) + 1) in rng D2
by A92, FUNCT_1:def 3;
then
D2 . ((indx (D2,D1,j1)) + 1) in {x}
by A4, A96, XBOOLE_0:def 3;
then A104:
D2 . ((indx (D2,D1,j1)) + 1) = x
by TARSKI:def 1;
D2 . (((indx (D2,D1,j1)) + 1) + 1) in rng D2
by A88, FUNCT_1:def 3;
then
D2 . (((indx (D2,D1,j1)) + 1) + 1) in {x}
by A4, A96, XBOOLE_0:def 3;
then
D2 . ((indx (D2,D1,j1)) + 1) = D2 . (((indx (D2,D1,j1)) + 1) + 1)
by A104, TARSKI:def 1;
hence
contradiction
by A84, A92, A88, SEQ_4:138;
verum
end;
A105:
len D1 <= len (lower_volume (g,D1))
by INTEGRA1:def 7;
A106:
1
<= len D1
by A69, FINSEQ_1:1;
then A107:
(mid ((lower_volume (g,D1)),(len D1),(len D1))) . 1
= (lower_volume (g,D1)) . (len D1)
by A105, FINSEQ_6:118;
reconsider lv =
(lower_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 ((lower_volume (g,D1)),(len D1),(len D1))) = 1
by A106, A105, FINSEQ_6:118;
then A108:
mid (
(lower_volume (g,D1)),
(len D1),
(len D1))
= <*lv*>
by A107, FINSEQ_1:40;
A109:
1
<= (indx (D2,D1,j1)) + 1
by A14, NAT_1:13;
indx (
D2,
D1,
(len D1))
in dom D2
by A3, A5, INTEGRA1:def 19;
then A110:
indx (
D2,
D1,
(len D1))
in Seg (len D2)
by FINSEQ_1:def 3;
then A111:
1
<= indx (
D2,
D1,
(len D1))
by FINSEQ_1:1;
indx (
D2,
D1,
(len D1))
in Seg (len (lower_volume (g,D2)))
by A110, INTEGRA1:def 7;
then A112:
indx (
D2,
D1,
(len D1))
<= len (lower_volume (g,D2))
by FINSEQ_1:1;
then A113:
(indx (D2,D1,j1)) + 1
<= len (lower_volume (g,D2))
by A79, XXREAL_0:2;
then
(indx (D2,D1,j1)) + 1
in Seg (len (lower_volume (g,D2)))
by A109, FINSEQ_1:1;
then A114:
(indx (D2,D1,j1)) + 1
in Seg (len D2)
by INTEGRA1:def 7;
(indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1) = (indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)
by A79, XREAL_1:233;
then
((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1
<= 2
by A82;
then A115:
len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= 2
by A79, A111, A112, A109, A113, FINSEQ_6:118;
len (lower_volume (g,D2)) = len D2
by INTEGRA1:def 7;
then A116:
(indx (D2,D1,j1)) + 1
in dom D2
by A109, A113, FINSEQ_3:25;
((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1
>= 0 + 1
by XREAL_1:6;
then A117:
1
<= len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))
by A79, A111, A112, A109, A113, FINSEQ_6:118;
now (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)per cases
( len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 1 or len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 2 )
by A117, A115, Lm2;
suppose A118:
len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 1
;
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
upper_bound (divset (D1,(len D1))) = D1 . (len D1)
by A5, A7, INTEGRA1:def 4;
then A119:
upper_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,(len D1)))
by A3, A5, INTEGRA1:def 19;
lower_bound (divset (D1,(len D1))) = D1 . j1
by A5, A7, INTEGRA1:def 4;
then
lower_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,j1))
by A3, A8, INTEGRA1:def 19;
then A120:
divset (
D1,
(len D1))
= [.(D2 . (indx (D2,D1,j1))),(D2 . (indx (D2,D1,(len D1)))).]
by A119, INTEGRA1:4;
A121:
delta D1 >= 0
by Th9;
A122:
(upper_bound (rng g)) - (lower_bound (rng g)) >= 0
by A72, Lm3, XREAL_1:48;
A123:
indx (
D2,
D1,
(len D1))
in dom D2
by A3, A5, INTEGRA1:def 19;
len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = ((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1
by A79, A111, A112, A109, A113, FINSEQ_6:118;
then A124:
(indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1) = 0
by A79, A118, XREAL_1:233;
then
indx (
D2,
D1,
(len D1))
<> 1
by A13, FINSEQ_3:25;
then A125:
upper_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . (indx (D2,D1,(len D1)))
by A123, INTEGRA1:def 4;
lower_bound (divset (D2,(indx (D2,D1,(len D1))))) = D2 . ((indx (D2,D1,(len D1))) - 1)
by A14, A124, A123, INTEGRA1:def 4;
then A126:
divset (
D2,
(indx (D2,D1,(len D1))))
= divset (
D1,
(len D1))
by A124, A120, A125, INTEGRA1:4;
reconsider li =
(lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1) as
Element of
REAL by XREAL_0:def 1;
(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1
= (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)
by A111, A112, A109, A113, FINSEQ_6:118;
then
mid (
(lower_volume (g,D2)),
((indx (D2,D1,j1)) + 1),
(indx (D2,D1,(len D1))))
= <*li*>
by A118, FINSEQ_1:40;
then Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) =
(lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)
by FINSOP_1:11
.=
(lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A116, INTEGRA1:def 7
.=
(lower_volume (g,D1)) . (len D1)
by A5, A124, A126, INTEGRA1:def 7
.=
Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))
by A108, FINSOP_1:11
;
hence
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A121, A122;
verum end; suppose A127:
len (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = 2
;
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)A128:
(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 1
= (lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)
by A111, A112, A109, A113, FINSEQ_6:118;
A129:
2
+ ((indx (D2,D1,j1)) + 1) >= 0 + 1
by XREAL_1:7;
(mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) . 2 =
H1(
D2)
. ((2 + ((indx (D2,D1,j1)) + 1)) -' 1)
by A79, A111, A112, A109, A113, A127, FINSEQ_6:118
.=
H1(
D2)
. ((2 + ((indx (D2,D1,j1)) + 1)) - 1)
by A129, XREAL_1:233
.=
H1(
D2)
. ((indx (D2,D1,j1)) + (1 + 1))
;
then
mid (
(lower_volume (g,D2)),
((indx (D2,D1,j1)) + 1),
(indx (D2,D1,(len D1))))
= <*((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)),((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 2))*>
by A127, A128, FINSEQ_1:44;
then A130:
Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) = ((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 1)) + ((lower_volume (g,D2)) . ((indx (D2,D1,j1)) + 2))
by RVSUM_1:77;
A131:
vol (divset (D2,((indx (D2,D1,j1)) + 1))) >= 0
by INTEGRA1:9;
upper_bound (divset (D1,(len D1))) = D1 . (len D1)
by A5, A7, INTEGRA1:def 4;
then A132:
upper_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,(len D1)))
by A3, A5, INTEGRA1:def 19;
A133:
vol (divset (D2,((indx (D2,D1,j1)) + 2))) >= 0
by INTEGRA1:9;
((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1
= 2
by A79, A111, A112, A109, A113, A127, FINSEQ_6:118;
then A134:
((indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)) + 1
= 2
by A79, XREAL_1:233;
then A135:
(indx (D2,D1,j1)) + 2
in dom D2
by A3, A5, INTEGRA1:def 19;
lower_bound (divset (D1,(len D1))) = D1 . j1
by A5, A7, INTEGRA1:def 4;
then
lower_bound (divset (D1,(len D1))) = D2 . (indx (D2,D1,j1))
by A3, A8, INTEGRA1:def 19;
then A136:
vol (divset (D1,(len D1))) = (((D2 . ((indx (D2,D1,j1)) + 2)) - (D2 . ((indx (D2,D1,j1)) + 1))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1)))
by A132, A134, INTEGRA1:def 5;
(indx (D2,D1,j1)) + 1
in Seg (len (lower_volume (g,D2)))
by A109, A113, FINSEQ_1:1;
then
(indx (D2,D1,j1)) + 1
in Seg (len D2)
by INTEGRA1:def 7;
then A137:
(indx (D2,D1,j1)) + 1
in dom D2
by FINSEQ_1:def 3;
A138:
(indx (D2,D1,j1)) + 1
<> 1
by A14, NAT_1:13;
then A139:
upper_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . ((indx (D2,D1,j1)) + 1)
by A137, INTEGRA1:def 4;
((indx (D2,D1,j1)) + 1) - 1
= (indx (D2,D1,j1)) + 0
;
then A140:
lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1))
by A137, A138, INTEGRA1:def 4;
A141:
((indx (D2,D1,j1)) + 1) + 1
> 1
by A109, NAT_1:13;
((indx (D2,D1,j1)) + 2) - 1
= (indx (D2,D1,j1)) + 1
;
then A142:
lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1)
by A135, A141, INTEGRA1:def 4;
upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2)
by A135, A141, INTEGRA1:def 4;
then vol (divset (D1,(len D1))) =
((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1)))
by A142, A136, INTEGRA1:def 5
.=
(vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + ((upper_bound (divset (D2,((indx (D2,D1,j1)) + 1)))) - (lower_bound (divset (D2,((indx (D2,D1,j1)) + 1)))))
by A140, A139
;
then A143:
vol (divset (D1,(len D1))) = (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by INTEGRA1:def 5;
then A144:
(lower_volume (g,D1)) . (len D1) = (lower_bound (rng (g | (divset (D1,(len D1)))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2)))))
by A5, INTEGRA1:def 7;
A145:
(Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H1(D1),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
proof
set ID1 =
(indx (D2,D1,j1)) + 1;
set ID2 =
(indx (D2,D1,j1)) + 2;
set IR =
(lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))));
divset (
D1,
(len D1))
c= A
by A5, INTEGRA1:8;
then A146:
lower_bound (rng (g | (divset (D1,(len D1))))) >= lower_bound (rng g)
by A72, Lm4;
Sum (mid (H1(D1),(len D1),(len D1))) = ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by A108, A144, FINSOP_1:11;
then
(Sum (mid (H1(D1),(len D1),(len D1)))) - ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by A133, A146, XREAL_1:64;
then
Sum (mid (H1(D1),(len D1),(len D1))) >= ((lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) + ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))))
by XREAL_1:19;
then A147:
(Sum (mid (H1(D1),(len D1),(len D1)))) - ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:19;
(lower_bound (rng (g | (divset (D1,(len D1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A131, A146, XREAL_1:64;
then
(Sum (mid (H1(D1),(len D1),(len D1)))) - ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A147, XXREAL_0:2;
then A148:
Sum (mid (H1(D1),(len D1),(len D1))) >= ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:19;
((indx (D2,D1,(len D1))) -' ((indx (D2,D1,j1)) + 1)) + 1
= 2
by A79, A111, A112, A109, A113, A127, FINSEQ_6:118;
then A149:
((indx (D2,D1,(len D1))) - ((indx (D2,D1,j1)) + 1)) + 1
= 2
by A79, XREAL_1:233;
(indx (D2,D1,j1)) + 1
in dom D2
by A114, FINSEQ_1:def 3;
then
divset (
D2,
((indx (D2,D1,j1)) + 1))
c= A
by INTEGRA1:8;
then
lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1))))) <= upper_bound (rng g)
by A72, Lm4;
then A150:
(lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A131, XREAL_1:64;
A151:
indx (
D2,
D1,
(len D1))
in dom D2
by A3, A5, INTEGRA1:def 19;
then
divset (
D2,
((indx (D2,D1,j1)) + 2))
c= A
by A149, INTEGRA1:8;
then A152:
lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2))))) <= upper_bound (rng g)
by A72, Lm4;
Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) =
((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + (H1(D2) . ((indx (D2,D1,j1)) + 1))
by A130, A151, A149, INTEGRA1:def 7
.=
((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by A116, INTEGRA1:def 7
;
then
(Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by A133, A152, XREAL_1:64;
then
Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:20;
then
(Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (lower_bound (rng (g | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:20;
then
(Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A150, XXREAL_0:2;
then
Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))) <= ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:20;
then
(Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H1(D1),(len D1),(len D1)))) <= (((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))) - (((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng g)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))))
by A148, XREAL_1:13;
hence
(Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid (H1(D1),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
;
verum
end;
(upper_bound (rng g)) - (lower_bound (rng g)) >= 0
by A72, Lm3, XREAL_1:48;
then
((upper_bound (rng g)) - (lower_bound (rng g))) * (vol (divset (D1,(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A5, Lm5, XREAL_1:64;
hence
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A143, A145, XXREAL_0:2;
verum end; end; end;
hence
(Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) - (Sum (mid ((lower_volume (g,D1)),(len D1),(len D1)))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
;
verum
end;
indx (D2,D1,j1) in dom D2
by A3, A12, INTEGRA1:def 19;
then
indx (D2,D1,j1) <= len D2
by FINSEQ_3:25;
then A153:
indx (D2,D1,j1) <= len (lower_volume (g,D2))
by INTEGRA1:def 7;
j1 <= len D1
by A12, FINSEQ_3:25;
then A154:
j1 <= len (lower_volume (g,D1))
by INTEGRA1:def 7;
A155:
D2 . (indx (D2,D1,(len D1))) = D1 . (len D1)
by A3, A5, INTEGRA1:def 19;
A156:
indx (D2,D1,(len D1)) >= len (lower_volume (g,D2))
proof
assume
indx (
D2,
D1,
(len D1))
< len (lower_volume (g,D2))
;
contradiction
then
indx (
D2,
D1,
(len D1))
< len D2
by INTEGRA1:def 7;
then A157:
D1 . (len D1) < D2 . (len D2)
by A66, A6, A155, SEQM_3:def 1;
A158:
not
D2 . (len D2) in rng D1
D2 . (len D2) in rng D2
by A66, FUNCT_1:def 3;
then
(
D2 . (len D2) in rng D1 or
D2 . (len D2) in {x} )
by A4, XBOOLE_0:def 3;
then
D2 . (len D2) = x
by A158, TARSKI:def 1;
then
D2 . (len D2) <= upper_bound (divset (D1,(len D1)))
by A1, INTEGRA2:1;
hence
contradiction
by A5, A7, A157, INTEGRA1:def 4;
verum
end;
indx (D2,D1,(len D1)) in Seg (len D2)
by A6, FINSEQ_1:def 3;
then
indx (D2,D1,(len D1)) in Seg (len (lower_volume (g,D2)))
by INTEGRA1:def 7;
then
indx (D2,D1,(len D1)) in dom (lower_volume (g,D2))
by FINSEQ_1:def 3;
then A159: H2(D2, indx (D2,D1,(len D1))) =
Sum ((lower_volume (g,D2)) | (indx (D2,D1,(len D1))))
by INTEGRA1:def 20
.=
Sum (lower_volume (g,D2))
by A156, FINSEQ_1:58
;
len D1 in Seg (len (lower_volume (g,D1)))
by A69, INTEGRA1:def 7;
then
len D1 in dom (lower_volume (g,D1))
by FINSEQ_1:def 3;
then A160: H2(D1, len D1) =
Sum ((lower_volume (g,D1)) | (len D1))
by INTEGRA1:def 20
.=
Sum (lower_volume (g,D1))
by A67, FINSEQ_1:58
;
len D1 = len (lower_volume (g,D1))
by INTEGRA1:def 7;
then A161:
j1 in dom (lower_volume (g,D1))
by A8, FINSEQ_3:29;
len (D2 | (indx (D2,D1,j1))) = len (D1 | j1)
by A15, A11, A18, Th6;
then
indx (D2,D1,j1) = j1
by A9, A17, FINSEQ_1:59;
then
len ((lower_volume (g,D1)) | j1) = indx (D2,D1,j1)
by A154, FINSEQ_1:59;
then
len ((lower_volume (g,D1)) | j1) = len ((lower_volume (g,D2)) | (indx (D2,D1,j1)))
by A153, FINSEQ_1:59;
then A162:
(lower_volume (g,D2)) | (indx (D2,D1,j1)) = (lower_volume (g,D1)) | j1
by A38, FINSEQ_1:14;
len D2 = len (lower_volume (g,D2))
by INTEGRA1:def 7;
then
indx (D2,D1,j1) in dom (lower_volume (g,D2))
by A13, FINSEQ_3:29;
then A163: H2(D2, indx (D2,D1,j1)) =
Sum ((lower_volume (g,D2)) | (indx (D2,D1,j1)))
by INTEGRA1:def 20
.=
H2(D1,j1)
by A162, A161, INTEGRA1:def 20
;
indx (D2,D1,(len D1)) <= len D2
by A76, FINSEQ_1:1;
then A164:
indx (D2,D1,(len D1)) <= len H1(D2)
by INTEGRA1:def 7;
A165:
len D2 = len H1(D2)
by INTEGRA1:def 7;
then A166:
indx (D2,D1,(len D1)) in dom H1(D2)
by A75, FINSEQ_3:29;
indx (D2,D1,j1) in dom H1(D2)
by A13, A165, FINSEQ_3:29;
then
H2(D2, indx (D2,D1,j1)) = Sum (H1(D2) | (indx (D2,D1,j1)))
by INTEGRA1:def 20;
then H2(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) =
Sum ((H1(D2) | (indx (D2,D1,j1))) ^ (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))))
by RVSUM_1:75
.=
Sum ((mid (H1(D2),1,(indx (D2,D1,j1)))) ^ (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1))))))
by A14, FINSEQ_6:116
.=
Sum (mid (H1(D2),1,(indx (D2,D1,(len D1)))))
by A14, A78, A164, INTEGRA2:4
.=
Sum (H1(D2) | (indx (D2,D1,(len D1))))
by A77, FINSEQ_6:116
;
then
H2(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (g,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,(len D1)))))) = H2(D2, indx (D2,D1,(len D1)))
by A166, INTEGRA1:def 20;
hence
(Sum (lower_volume (g,D2))) - (Sum (lower_volume (g,D1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta D1)
by A163, A81, A74, A159, A160; verum