let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,REAL; :: thesis:
assume A1: f | A is bounded ; :: thesis:
then A5: for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by Th20;
for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds
ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

let D, D1 be Division of A; :: thesis:
assume A11: delta D1 < min (rng (upper_volume ((chi (A,A)),D))) ; :: thesis:
ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

consider D2 being Division of A such that
A12: D <= D2 and
A13: D1 <= D2 and
A14: rng D2 = (rng D1) \/ (rng D) and
0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) and
0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) by A5;
(lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

deffunc H₁( Division of A) -> FinSequence of REAL = lower_volume (f,$1);
deffunc H₂( Division of A, Nat) -> set = (PartSums (lower_volume (f,$1))) . $2;
A15: len D2 in dom D2 by FINSEQ_5:6;
A16: for i being Element of NAT st i in dom D holds
ex j being Element of NAT st
( j in dom D1 & D . i in divset (D1,j) & H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

defpred S₁[ non zero Nat] means ( $1 in dom D implies ex j being Element of NAT st
( j in dom D1 & D . $1 in divset (D1,j) & H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= ($1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) );
let i be Element of NAT ; :: thesis:
assume A17: i in dom D ; :: thesis:
then A18: i in Seg (len D) by FINSEQ_1:def 3;
A19: for i, j being Element of NAT st i in dom D & j in dom D1 & D . i in divset (D1,j) holds
j >= 2

proof

let i, j be Element of NAT ; :: thesis:
assume A20: i in dom D ; :: thesis:
assume that
A21: j in dom D1 and
A22: D . i in divset (D1,j) ; :: thesis:
assume j < 2 ; :: thesis:
then j < 1 + 1 ;
then A23: j <= 1 by NAT_1:13;
j in Seg (len D1) by A21, FINSEQ_1:def 3;
then j >= 1 by FINSEQ_1:1;
then j = 1 by A23, XXREAL_0:1;
then A24: lower_bound (divset (D1,j)) = lower_bound A by A21, INTEGRA1:def 4;
A25: D . i <= upper_bound (divset (D1,j)) by A22, INTEGRA2:1;
delta D1 >= min (rng (upper_volume ((chi (A,A)),D)))

proof

per cases ;

suppose A26: i = 1 ; :: thesis:

len D in Seg (len D) by FINSEQ_1:3;
then 1 <= len D by FINSEQ_1:1;
then A27: 1 in Seg (len D) by FINSEQ_1:1;
then A28: 1 in dom D by FINSEQ_1:def 3;
then A29: lower_bound (divset (D,1)) = lower_bound A by INTEGRA1:def 4;
1 in Seg (len (upper_volume ((chi (A,A)),D))) by A27, INTEGRA1:def 6;
then A30: 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
vol (divset (D,1)) = (upper_volume ((chi (A,A)),D)) . 1 by A28, INTEGRA1:20;
then vol (divset (D,1)) in rng (upper_volume ((chi (A,A)),D)) by A30, FUNCT_1:def 3;
then A31: vol (divset (D,1)) >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;
A32: upper_bound (divset (D,1)) = D . 1 by A28, INTEGRA1:def 4;
(upper_bound (divset (D1,j))) - (lower_bound A) >= (D . 1) - (lower_bound A) by A25, A26, XREAL_1:9;
then vol (divset (D1,j)) >= (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by A24, A29, A32, INTEGRA1:def 5;
then A33: vol (divset (D1,j)) >= vol (divset (D,1)) by INTEGRA1:def 5;
vol (divset (D1,j)) <= delta D1 by A21, Lm5;
then delta D1 >= vol (divset (D,1)) by A33, XXREAL_0:2;
hence delta D1 >= min (rng (upper_volume ((chi (A,A)),D))) by A31, XXREAL_0:2; :: thesis:

end;

suppose A34: i <> 1 ; :: thesis:

then D . (i - 1) in A by A20, INTEGRA1:7;
then A35: lower_bound A <= D . (i - 1) by INTEGRA2:1;
lower_bound (divset (D,i)) = D . (i - 1) by A20, A34, INTEGRA1:def 4;
then A36: (upper_bound (divset (D,i))) - (lower_bound A) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A35, XREAL_1:10;
upper_bound (divset (D,i)) = D . i by A20, A34, INTEGRA1:def 4;
then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound A) by A25, A24, XREAL_1:9;
then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A36, XXREAL_0:2;
then vol (divset (D1,j)) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by INTEGRA1:def 5;
then A37: vol (divset (D1,j)) >= vol (divset (D,i)) by INTEGRA1:def 5;
i in Seg (len D) by A20, FINSEQ_1:def 3;
then i in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;
then A38: i in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
vol (divset (D,i)) = (upper_volume ((chi (A,A)),D)) . i by A20, INTEGRA1:20;
then vol (divset (D,i)) in rng (upper_volume ((chi (A,A)),D)) by A38, FUNCT_1:def 3;
then A39: vol (divset (D,i)) >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;
vol (divset (D1,j)) <= delta D1 by A21, Lm5;
then delta D1 >= vol (divset (D,i)) by A37, XXREAL_0:2;
hence delta D1 >= min (rng (upper_volume ((chi (A,A)),D))) by A39, XXREAL_0:2; :: thesis:

end;

hence contradiction by A11; :: thesis:

end;

A40: S₁[1]

proof

len D in Seg (len D) by FINSEQ_1:3;
then 1 <= len D by FINSEQ_1:1;
then A41: 1 in dom D by FINSEQ_3:25;
then consider j being Element of NAT such that
A42: j in dom D1 and
A43: D . 1 in divset (D1,j) by Th3, INTEGRA1:6;
H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

A44: j <> 1 by A19, A41, A42, A43;
then reconsider j1 = j - 1 as Element of NAT by A42, INTEGRA1:7;
A45: j1 in dom D1 by A42, A44, INTEGRA1:7;
then j1 in Seg (len D1) by FINSEQ_1:def 3;
then j1 in Seg (len (lower_volume (f,D1))) by INTEGRA1:def 7;
then A46: j1 in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;
A47: j - 1 in dom D1 by A42, A44, INTEGRA1:7;
then A48: indx (D2,D1,j1) in dom D2 by A13, INTEGRA1:def 19;
then A49: indx (D2,D1,j1) in Seg (len D2) by FINSEQ_1:def 3;
then A50: 1 <= indx (D2,D1,j1) by FINSEQ_1:1;
then mid (D2,1,(indx (D2,D1,j1))) is increasing by A48, INTEGRA1:35;
then A51: D2 | (indx (D2,D1,j1)) is increasing by A50, FINSEQ_6:116;
j < j + 1 by NAT_1:13;
then j1 < j by XREAL_1:19;
then A52: indx (D2,D1,j1) < indx (D2,D1,j) by A13, A42, A45, Th8;
then A53: (indx (D2,D1,j1)) + 1 <= indx (D2,D1,j) by NAT_1:13;
A54: (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid ((lower_volume (f,D1)),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof

A55: (indx (D2,D1,j)) - (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,j)) - (indx (D2,D1,j1)) > 2 ; :: thesis:
then A56: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,j) by XREAL_1:20;
A57: ID1 < ID2 by NAT_1:13;
then indx (D2,D1,j1) <= ID2 by NAT_1:13;
then A58: 1 <= ID2 by A50, XXREAL_0:2;
A59: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;
then A60: indx (D2,D1,j) <= len D2 by FINSEQ_3:25;
then ID2 <= len D2 by A56, XXREAL_0:2;
then ID2 in Seg (len D2) by A58, FINSEQ_1:1;
then A61: ID2 in dom D2 by FINSEQ_1:def 3;
then A62: D2 . ID2 < D2 . (indx (D2,D1,j)) by A56, A59, SEQM_3:def 1;
A63: 1 <= ID1 by A50, NAT_1:13;
A64: D1 . j = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;
ID1 <= indx (D2,D1,j) by A56, A57, XXREAL_0:2;
then ID1 <= len D2 by A60, XXREAL_0:2;
then ID1 in Seg (len D2) by A63, FINSEQ_1:1;
then A65: ID1 in dom D2 by FINSEQ_1:def 3;
then A66: D2 . ID1 < D2 . ID2 by A57, A61, SEQM_3:def 1;
indx (D2,D1,j1) < ID1 by NAT_1:13;
then A67: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A48, A65, SEQM_3:def 1;
A68: D1 . j1 = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;
A69: ( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

proof

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

per cases by A70;

suppose D2 . ID1 in rng D1 ; :: thesis:

then consider n being Element of NAT such that
A71: n in dom D1 and
A72: D1 . n = D2 . ID1 by PARTFUN1:3;
j1 < n by A45, A67, A68, A71, A72, SEQ_4:137;
then A73: j < n + 1 by XREAL_1:19;
D2 . ID1 < D2 . (indx (D2,D1,j)) by A66, A62, XXREAL_0:2;
then n < j by A42, A64, A71, A72, SEQ_4:137;
hence contradiction by A73, NAT_1:13; :: thesis:

end;

suppose D2 . ID2 in rng D1 ; :: thesis:

then consider n being Element of NAT such that
A74: n in dom D1 and
A75: D1 . n = D2 . ID2 by PARTFUN1:3;
D2 . (indx (D2,D1,j1)) < D2 . ID2 by A67, A66, XXREAL_0:2;
then j1 < n by A45, A68, A74, A75, SEQ_4:137;
then A76: j < n + 1 by XREAL_1:19;
n < j by A42, A62, A64, A74, A75, SEQ_4:137;
hence contradiction by A76, NAT_1:13; :: thesis:

end;

upper_bound (divset (D1,j)) = D1 . j by A42, A44, INTEGRA1:def 4;
then A77: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;
lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;
then A78: lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;
D2 . ID2 in (rng D) \/ (rng D1) by A14, A61, FUNCT_1:def 3;
then A79: D2 . ID2 in rng D by A69, XBOOLE_0:def 3;
D2 . ID1 in (rng D) \/ (rng D1) by A14, A65, FUNCT_1:def 3;
then A80: D2 . ID1 in rng D by A69, XBOOLE_0:def 3;
D2 . (indx (D2,D1,j1)) <= D2 . ID2 by A67, A66, XXREAL_0:2;
then D2 . ID2 in divset (D1,j) by A62, A78, A77, INTEGRA2:1;
then A81: D2 . ID2 in (rng D) /\ (divset (D1,j)) by A79, XBOOLE_0:def 4;
D2 . ID1 <= D2 . (indx (D2,D1,j)) by A66, A62, XXREAL_0:2;
then D2 . ID1 in divset (D1,j) by A67, A78, A77, INTEGRA2:1;
then D2 . ID1 in (rng D) /\ (divset (D1,j)) by A80, XBOOLE_0:def 4;
hence contradiction by A11, A42, A57, A65, A61, A81, Th5, SEQ_4:138; :: thesis:

end;

A82: 1 <= (indx (D2,D1,j1)) + 1 by A50, NAT_1:13;
j <= len D1 by A42, FINSEQ_3:25;
then A83: j <= len (lower_volume (f,D1)) by INTEGRA1:def 7;
A84: 1 <= j by A42, FINSEQ_3:25;
then A85: (mid ((lower_volume (f,D1)),j,j)) . 1 = (lower_volume (f,D1)) . j by A83, FINSEQ_6:118;
reconsider lv = (lower_volume (f,D1)) . j as Element of REAL by XREAL_0:def 1;
(j -' j) + 1 = 1 by Lm1;
then len (mid ((lower_volume (f,D1)),j,j)) = 1 by A84, A83, FINSEQ_6:118;
then mid ((lower_volume (f,D1)),j,j) = <*lv*> by A85, FINSEQ_1:40;
then A86: Sum (mid ((lower_volume (f,D1)),j,j)) = (lower_volume (f,D1)) . j by FINSOP_1:11;
indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;
then A87: indx (D2,D1,j) in Seg (len D2) by FINSEQ_1:def 3;
then A88: 1 <= indx (D2,D1,j) by FINSEQ_1:1;
indx (D2,D1,j) in Seg (len (lower_volume (f,D2))) by A87, INTEGRA1:def 7;
then A89: indx (D2,D1,j) <= len (lower_volume (f,D2)) by FINSEQ_1:1;
then A90: (indx (D2,D1,j1)) + 1 <= len (lower_volume (f,D2)) by A53, XXREAL_0:2;
then (indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (f,D2))) by A82, FINSEQ_1:1;
then A91: (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;
then A92: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;
(indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1) = (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) by A53, XREAL_1:233;
then ((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 <= 2 by A55;
then A93: len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= 2 by A53, A88, A89, A82, A90, FINSEQ_6:118;
((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 >= 0 + 1 by XREAL_1:6;
then A94: 1 <= len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) by A53, A88, A89, A82, A90, FINSEQ_6:118;

now :: thesis:

per cases by A94, A93, Lm2;

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

upper_bound (divset (D1,j)) = D1 . j by A42, A44, INTEGRA1:def 4;
then A96: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;
lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;
then lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;
then A97: divset (D1,j) = [.(D2 . (indx (D2,D1,j1))),(D2 . (indx (D2,D1,j))).] by A96, INTEGRA1:4;
A98: delta D1 >= 0 by Th9;
A99: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
A100: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;
((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 1 by A53, A88, A89, A82, A90, A95, FINSEQ_6:118;
then A101: (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) = 0 by A53, XREAL_1:233;
then indx (D2,D1,j) <> 1 by A49, FINSEQ_1:1;
then A102: upper_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j)) by A100, INTEGRA1:def 4;
(indx (D2,D1,j)) - 1 = indx (D2,D1,j1) by A101;
then lower_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j1)) by A50, A101, A100, INTEGRA1:def 4;
then A103: divset (D2,(indx (D2,D1,j))) = divset (D1,j) by A97, A102, INTEGRA1:4;
reconsider lv = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) as Element of REAL by XREAL_0:def 1;
(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by A88, A89, A82, A90, FINSEQ_6:118;
then mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*lv*> by A95, FINSEQ_1:40;
then Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by FINSOP_1:11
.= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A92, INTEGRA1:def 7
.= Sum (mid ((lower_volume (f,D1)),j,j)) by A42, A86, A101, A103, INTEGRA1:def 7 ;
hence (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid ((lower_volume (f,D1)),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A98, A99; :: thesis:

end;

suppose A104: len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = 2 ; :: thesis:

A105: (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by A88, A89, A82, A90, FINSEQ_6:118;
A106: 2 + ((indx (D2,D1,j1)) + 1) >= 0 + 1 by XREAL_1:7;
(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 2 = H₁(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1) by A53, A88, A89, A82, A90, A104, FINSEQ_6:118
.= H₁(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) - 1) by A106, XREAL_1:233
.= H₁(D2) . ((indx (D2,D1,j1)) + (1 + 1)) ;
then mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)),((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 2))*> by A104, A105, FINSEQ_1:44;
then A107: Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = ((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)) + ((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 2)) by RVSUM_1:77;
A108: vol (divset (D2,((indx (D2,D1,j1)) + 1))) >= 0 by INTEGRA1:9;
upper_bound (divset (D1,j)) = D1 . j by A42, A44, INTEGRA1:def 4;
then A109: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;
A110: vol (divset (D2,((indx (D2,D1,j1)) + 2))) >= 0 by INTEGRA1:9;
((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, A88, A89, A82, A90, A104, FINSEQ_6:118;
then A111: ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, XREAL_1:233;
then A112: (indx (D2,D1,j1)) + 2 in dom D2 by A13, A42, INTEGRA1:def 19;
lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;
then lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;
then A113: vol (divset (D1,j)) = (((D2 . ((indx (D2,D1,j1)) + 2)) - (D2 . ((indx (D2,D1,j1)) + 1))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A109, A111, INTEGRA1:def 5;
(indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (f,D2))) by A82, A90, FINSEQ_1:1;
then (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;
then A114: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;
A115: (indx (D2,D1,j1)) + 1 <> 1 by A50, NAT_1:13;
then A116: upper_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . ((indx (D2,D1,j1)) + 1) by A114, INTEGRA1:def 4;
((indx (D2,D1,j1)) + 1) - 1 = (indx (D2,D1,j1)) + 0 ;
then A117: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A114, A115, INTEGRA1:def 4;
A118: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A82, NAT_1:13;
((indx (D2,D1,j1)) + 2) - 1 = (indx (D2,D1,j1)) + 1 ;
then A119: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A112, A118, INTEGRA1:def 4;
upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A112, A118, INTEGRA1:def 4;
then vol (divset (D1,j)) = ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A119, A113, 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 A117, A116 ;
then A120: vol (divset (D1,j)) = (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by INTEGRA1:def 5;
then A121: (lower_volume (f,D1)) . j = (lower_bound (rng (f | (divset (D1,j))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A42, INTEGRA1:def 7;
A122: (Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))

proof

set ID2 = (indx (D2,D1,j1)) + 2;
set ID1 = (indx (D2,D1,j1)) + 1;
set B = vol (divset (D2,((indx (D2,D1,j1)) + 1)));
set C = vol (divset (D2,((indx (D2,D1,j1)) + 2)));
divset (D1,j) c= A by A42, INTEGRA1:8;
then A123: lower_bound (rng (f | (divset (D1,j)))) >= lower_bound (rng f) by A1, Lm4;
(indx (D2,D1,j1)) + 1 in dom D2 by A91, FINSEQ_1:def 3;
then divset (D2,((indx (D2,D1,j1)) + 1)) c= A by INTEGRA1:8;
then lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1))))) <= upper_bound (rng f) by A1, Lm4;
then A124: (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A108, XREAL_1:64;
((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, A88, A89, A82, A90, A104, FINSEQ_6:118;
then A125: ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, XREAL_1:233;
A126: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;
then divset (D2,((indx (D2,D1,j1)) + 2)) c= A by A125, INTEGRA1:8;
then A127: lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2))))) <= upper_bound (rng f) by A1, Lm4;
reconsider A = lower_bound (rng (f | (divset (D1,j)))) as Real ;
A128: ((lower_volume (f,D1)) . j) - (A * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = A * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A121;
(lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A110, A123, XREAL_1:64;
then Sum (mid (H₁(D1),j,j)) >= ((lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A86, A128, XREAL_1:19;
then A129: (Sum (mid (H₁(D1),j,j))) - ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by XREAL_1:19;
(lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A108, A123, XREAL_1:64;
then (Sum (mid (H₁(D1),j,j))) - ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A129, XXREAL_0:2;
then A130: Sum (mid (H₁(D1),j,j)) >= ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by XREAL_1:19;
Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + (H₁(D2) . ((indx (D2,D1,j1)) + 1)) by A107, A126, A125, INTEGRA1:def 7
.= ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A92, INTEGRA1:def 7 ;
then (Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A110, A127, XREAL_1:64;
then Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by XREAL_1:20;
then (Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by XREAL_1:20;
then (Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A124, XXREAL_0:2;
then Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by XREAL_1:20;
then (Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),j,j))) <= (((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))) - (((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))) by A130, XREAL_1:13;
hence (Sum (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) ; :: thesis:

end;

(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
then ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A42, Lm5, XREAL_1:64;
hence (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid ((lower_volume (f,D1)),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A120, A122, XXREAL_0:2; :: thesis:

end;

hence (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid ((lower_volume (f,D1)),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) ; :: thesis:

end;

j < j + 1 by NAT_1:13;
then A131: j1 < j by XREAL_1:19;
indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;
then A132: indx (D2,D1,j) in Seg (len D2) by FINSEQ_1:def 3;
then A133: 1 <= indx (D2,D1,j) by FINSEQ_1:1;
A134: indx (D2,D1,j1) <= len D2 by A49, FINSEQ_1:1;
then A135: len (D2 | (indx (D2,D1,j1))) = indx (D2,D1,j1) by FINSEQ_1:59;
A136: j1 in Seg (len D1) by A47, FINSEQ_1:def 3;
then A137: j1 <= len D1 by FINSEQ_1:1;
for x1 being object st x1 in rng (D1 | j1) holds
x1 in rng (D2 | (indx (D2,D1,j1)))

proof

let x1 be object ; :: thesis:
assume x1 in rng (D1 | j1) ; :: thesis:
then consider k being Element of NAT such that
A138: k in dom (D1 | j1) and
A139: x1 = (D1 | j1) . k by PARTFUN1:3;
k in Seg (len (D1 | j1)) by A138, FINSEQ_1:def 3;
then A140: k in Seg j1 by A137, FINSEQ_1:59;
then A141: k in dom D1 by A45, RFINSEQ:6;
k <= j1 by A140, FINSEQ_1:1;
then D1 . k <= D1 . j1 by A47, A141, SEQ_4:137;
then D2 . (indx (D2,D1,k)) <= D1 . j1 by A13, A141, INTEGRA1:def 19;
then A142: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by A13, A47, INTEGRA1:def 19;
A143: (D1 | j1) . k = D1 . k by A45, A140, RFINSEQ:6;
D1 . k in rng D1 by A141, FUNCT_1:def 3;
then x1 in rng D2 by A14, A139, A143, XBOOLE_0:def 3;
then consider n being Element of NAT such that
A144: n in dom D2 and
A145: x1 = D2 . n by PARTFUN1:3;
D2 . (indx (D2,D1,k)) = D2 . n by A13, A139, A143, A141, A145, INTEGRA1:def 19;
then A146: n <= indx (D2,D1,j1) by A48, A144, A142, SEQM_3:def 1;
1 <= n by A144, FINSEQ_3:25;
then A147: n in Seg (indx (D2,D1,j1)) by A146, FINSEQ_1:1;
then n in Seg (len (D2 | (indx (D2,D1,j1)))) by A134, FINSEQ_1:59;
then A148: n in dom (D2 | (indx (D2,D1,j1))) by FINSEQ_1:def 3;
D2 . n = (D2 | (indx (D2,D1,j1))) . n by A48, A147, RFINSEQ:6;
hence x1 in rng (D2 | (indx (D2,D1,j1))) by A145, A148, FUNCT_1:def 3; :: thesis:

end;

then A149: rng (D1 | j1) c= rng (D2 | (indx (D2,D1,j1))) ;
A150: 1 <= j1 by A136, FINSEQ_1:1;
lower_bound (divset (D1,j)) <= D . 1 by A43, INTEGRA2:1;
then A151: D1 . j1 <= D . 1 by A42, A44, INTEGRA1:def 4;
for x1 being object st x1 in rng (D2 | (indx (D2,D1,j1))) holds
x1 in rng (D1 | j1)

proof

let x1 be object ; :: thesis:
assume x1 in rng (D2 | (indx (D2,D1,j1))) ; :: thesis:
then consider k being Element of NAT such that
A152: k in dom (D2 | (indx (D2,D1,j1))) and
A153: x1 = (D2 | (indx (D2,D1,j1))) . k by PARTFUN1:3;
k in Seg (len (D2 | (indx (D2,D1,j1)))) by A152, FINSEQ_1:def 3;
then A154: k in Seg (indx (D2,D1,j1)) by A134, FINSEQ_1:59;
then A155: k in dom D2 by A48, RFINSEQ:6;
A156: len (D1 | j1) = j1 by A137, FINSEQ_1:59;
k <= indx (D2,D1,j1) by A154, FINSEQ_1:1;
then D2 . k <= D2 . (indx (D2,D1,j1)) by A48, A155, SEQ_4:137;
then A157: D2 . k <= D1 . j1 by A13, A47, INTEGRA1:def 19;
A158: ( D2 . k in rng D1 implies D2 . k in rng (D1 | j1) )

proof

assume D2 . k in rng D1 ; :: thesis:
then consider m being Element of NAT such that
A159: m in dom D1 and
A160: D2 . k = D1 . m by PARTFUN1:3;
m in Seg (len D1) by A159, FINSEQ_1:def 3;
then A161: 1 <= m by FINSEQ_1:1;
A162: m <= j1 by A45, A157, A159, A160, SEQM_3:def 1;
then m in Seg j1 by A161, FINSEQ_1:1;
then A163: D2 . k = (D1 | j1) . m by A45, A160, RFINSEQ:6;
m in dom (D1 | j1) by A156, A161, A162, FINSEQ_3:25;
hence D2 . k in rng (D1 | j1) by A163, FUNCT_1:def 3; :: thesis:

end;

A164: ( D2 . k in rng D implies D2 . k = D1 . j1 )

proof

assume D2 . k in rng D ; :: thesis:
then consider n being Element of NAT such that
A165: n in dom D and
A166: D2 . k = D . n by PARTFUN1:3;
1 <= n by A165, FINSEQ_3:25;
then D . 1 <= D2 . k by A41, A165, A166, SEQ_4:137;
then D1 . j1 <= D2 . k by A151, XXREAL_0:2;
hence D2 . k = D1 . j1 by A157, XXREAL_0:1; :: thesis:

end;

A167: ( D2 . k in rng D implies D2 . k in rng (D1 | j1) )

proof

j1 in Seg (len (D1 | j1)) by A150, A156, FINSEQ_1:1;
then j1 in dom (D1 | j1) by FINSEQ_1:def 3;
then A168: (D1 | j1) . j1 in rng (D1 | j1) by FUNCT_1:def 3;
assume A169: D2 . k in rng D ; :: thesis:
j1 in Seg j1 by A150, FINSEQ_1:1;
hence D2 . k in rng (D1 | j1) by A45, A164, A169, A168, RFINSEQ:6; :: thesis:

end;

D2 . k in rng D2 by A155, FUNCT_1:def 3;
hence x1 in rng (D1 | j1) by A14, A48, A153, A154, A167, A158, RFINSEQ:6, XBOOLE_0:def 3; :: thesis:

end;

then rng (D2 | (indx (D2,D1,j1))) c= rng (D1 | j1) ;
then A170: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A149, XBOOLE_0:def 10;
mid (D1,1,j1) is increasing by A42, A44, A150, INTEGRA1:7, INTEGRA1:35;
then A171: D1 | j1 is increasing by A150, FINSEQ_6:116;
then A172: D2 | (indx (D2,D1,j1)) = D1 | j1 by A51, A170, Th6;
A173: for k being Element of NAT st 1 <= k & k <= j1 holds
k = indx (D2,D1,k)

proof

let k be Element of NAT ; :: thesis:
assume that
A174: 1 <= k and
A175: k <= j1 ; :: thesis:
assume A176: k <> indx (D2,D1,k) ; :: thesis:

now :: thesis:

per cases by A176, XXREAL_0:1;

suppose A177: k > indx (D2,D1,k) ; :: thesis:

k <= len D1 by A137, A175, XXREAL_0:2;
then A178: k in dom D1 by A174, FINSEQ_3:25;
then indx (D2,D1,k) in dom D2 by A13, INTEGRA1:def 19;
then indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;
then A179: 1 <= indx (D2,D1,k) by FINSEQ_1:1;
A180: indx (D2,D1,k) < j1 by A175, A177, XXREAL_0:2;
then A181: indx (D2,D1,k) in Seg j1 by A179, FINSEQ_1:1;
indx (D2,D1,k) <= indx (D2,D1,j1) by A13, A45, A175, A178, Th7;
then indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A179, FINSEQ_1:1;
then A182: (D2 | (indx (D2,D1,j1))) . (indx (D2,D1,k)) = D2 . (indx (D2,D1,k)) by A48, RFINSEQ:6;
indx (D2,D1,k) <= len D1 by A137, A180, XXREAL_0:2;
then indx (D2,D1,k) in dom D1 by A179, FINSEQ_3:25;
then A183: D1 . k > D1 . (indx (D2,D1,k)) by A177, A178, SEQM_3:def 1;
D1 . k = D2 . (indx (D2,D1,k)) by A13, A178, INTEGRA1:def 19;
hence contradiction by A45, A172, A182, A183, A181, RFINSEQ:6; :: thesis:

end;

suppose A184: k < indx (D2,D1,k) ; :: thesis:

k <= len D1 by A137, A175, XXREAL_0:2;
then A185: k in dom D1 by A174, FINSEQ_3:25;
then indx (D2,D1,k) <= indx (D2,D1,j1) by A13, A45, A175, Th7;
then A186: k <= indx (D2,D1,j1) by A184, XXREAL_0:2;
then k <= len D2 by A134, XXREAL_0:2;
then A187: k in dom D2 by A174, FINSEQ_3:25;
k in Seg j1 by A174, A175, FINSEQ_1:1;
then A188: D1 . k = (D1 | j1) . k by A47, RFINSEQ:6;
indx (D2,D1,k) in dom D2 by A13, A185, INTEGRA1:def 19;
then A189: D2 . k < D2 . (indx (D2,D1,k)) by A184, A187, SEQM_3:def 1;
A190: k in Seg (indx (D2,D1,j1)) by A174, A186, FINSEQ_1:1;
D1 . k = D2 . (indx (D2,D1,k)) by A13, A185, INTEGRA1:def 19;
hence contradiction by A48, A172, A188, A189, A190, RFINSEQ:6; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A191: for k being Nat st 1 <= k & k <= len ((lower_volume (f,D1)) | j1) holds
((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k

proof

indx (D2,D1,j1) in Seg (len D2) by A48, FINSEQ_1:def 3;
then indx (D2,D1,j1) in Seg (len (lower_volume (f,D2))) by INTEGRA1:def 7;
then A192: indx (D2,D1,j1) in dom (lower_volume (f,D2)) by FINSEQ_1:def 3;
let k be Nat; :: thesis:
assume that
A193: 1 <= k and
A194: k <= len ((lower_volume (f,D1)) | j1) ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A195: len (lower_volume (f,D1)) = len D1 by INTEGRA1:def 7;
then A196: k <= j1 by A137, A194, FINSEQ_1:59;
then k <= len D1 by A137, XXREAL_0:2;
then A197: k in Seg (len D1) by A193, FINSEQ_1:1;
then A198: k in dom D1 by FINSEQ_1:def 3;
then A199: indx (D2,D1,k) in dom D2 by A13, INTEGRA1:def 19;
A200: k in Seg j1 by A193, A196, FINSEQ_1:1;
then indx (D2,D1,k) in Seg j1 by A173, A193, A196;
then A201: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A150, A173;
then indx (D2,D1,k) <= indx (D2,D1,j1) by FINSEQ_1:1;
then A202: indx (D2,D1,k) <= len D2 by A134, XXREAL_0:2;
A203: D1 . k = D2 . (indx (D2,D1,k)) by A13, A198, INTEGRA1:def 19;
A204: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

proof

per cases ;

suppose A205: k = 1 ; :: thesis:

then A206: upper_bound (divset (D1,k)) = D1 . k by A198, INTEGRA1:def 4;
A207: lower_bound (divset (D1,k)) = lower_bound A by A198, A205, INTEGRA1:def 4;
indx (D2,D1,k) = 1 by A150, A173, A205;
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 A199, A203, A207, A206, INTEGRA1:def 4; :: thesis:

end;

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

then reconsider k1 = k - 1 as Element of NAT by A198, INTEGRA1:7;
k <= k + 1 by NAT_1:11;
then k1 <= k by XREAL_1:20;
then A209: k1 <= j1 by A196, XXREAL_0:2;
A210: k - 1 in dom D1 by A198, A208, INTEGRA1:7;
then k1 in Seg (len D1) by FINSEQ_1:def 3;
then 1 <= k1 by FINSEQ_1:1;
then k1 = indx (D2,D1,k1) by A173, A209;
then A211: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A173, A193, A196;
A212: indx (D2,D1,k) <> 1 by A173, A193, A196, A208;
then A213: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A199, INTEGRA1:def 4;
A214: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A199, A212, INTEGRA1:def 4;
A215: upper_bound (divset (D1,k)) = D1 . k by A198, A208, INTEGRA1:def 4;
lower_bound (divset (D1,k)) = D1 . (k - 1) by A198, A208, INTEGRA1:def 4;
hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A13, A198, A215, A210, A213, A214, A211, INTEGRA1:def 19; :: thesis:

end;

divset (D2,(indx (D2,D1,k))) = [.(lower_bound (divset (D2,(indx (D2,D1,k))))),(upper_bound (divset (D2,(indx (D2,D1,k))))).] by INTEGRA1:4;
then A216: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A204, INTEGRA1:4;
A217: k in dom D1 by A197, FINSEQ_1:def 3;
j1 in Seg (len (lower_volume (f,D1))) by A45, A195, FINSEQ_1:def 3;
then j1 in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;
then A218: ((lower_volume (f,D1)) | j1) . k = (lower_volume (f,D1)) . k by A200, RFINSEQ:6
.= (lower_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A217, A216, INTEGRA1:def 7 ;
1 <= indx (D2,D1,k) by A173, A193, A196;
then indx (D2,D1,k) in Seg (len D2) by A202, FINSEQ_1:1;
then A219: indx (D2,D1,k) in dom D2 by FINSEQ_1:def 3;
((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A173, A193, A196
.= (lower_volume (f,D2)) . (indx (D2,D1,k)) by A201, A192, RFINSEQ:6
.= (lower_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A219, INTEGRA1:def 7 ;
hence ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k by A218; :: thesis:

end;

indx (D2,D1,j1) in dom D2 by A13, A47, INTEGRA1:def 19;
then indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;
then A220: indx (D2,D1,j1) <= len (lower_volume (f,D2)) by INTEGRA1:def 7;
j1 <= len D1 by A47, FINSEQ_3:25;
then A221: j1 <= len (lower_volume (f,D1)) by INTEGRA1:def 7;
len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A51, A171, A170, Th6;
then indx (D2,D1,j1) = j1 by A137, A135, FINSEQ_1:59;
then len ((lower_volume (f,D1)) | j1) = indx (D2,D1,j1) by A221, FINSEQ_1:59;
then len ((lower_volume (f,D1)) | j1) = len ((lower_volume (f,D2)) | (indx (D2,D1,j1))) by A220, FINSEQ_1:59;
then A222: (lower_volume (f,D2)) | (indx (D2,D1,j1)) = (lower_volume (f,D1)) | j1 by A191, FINSEQ_1:14;
A223: j in Seg (len D1) by A42, FINSEQ_1:def 3;
then A224: 1 <= j by FINSEQ_1:1;
indx (D2,D1,j) in Seg (len H₁(D2)) by A132, INTEGRA1:def 7;
then A225: indx (D2,D1,j) in dom H₁(D2) by FINSEQ_1:def 3;
indx (D2,D1,j) <= len D2 by A132, FINSEQ_1:1;
then A226: indx (D2,D1,j) <= len H₁(D2) by INTEGRA1:def 7;
j in Seg (len H₁(D1)) by A223, INTEGRA1:def 7;
then A227: j in dom H₁(D1) by FINSEQ_1:def 3;
j <= len D1 by A223, FINSEQ_1:1;
then A228: j <= len H₁(D1) by INTEGRA1:def 7;
j1 in Seg (len D1) by A45, 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 20;
then H₂(D1,j1) + (Sum (mid (H₁(D1),j,j))) = Sum ((H₁(D1) | j1) ^ (mid (H₁(D1),j,j))) by RVSUM_1:75
.= Sum ((mid (H₁(D1),1,j1)) ^ (mid (H₁(D1),(j1 + 1),j))) by A150, FINSEQ_6:116
.= Sum (mid (H₁(D1),1,j)) by A150, A228, A131, INTEGRA2:4
.= Sum (H₁(D1) | j) by A224, FINSEQ_6:116 ;
then A229: H₂(D1,j1) + (Sum (mid ((lower_volume (f,D1)),j,j))) = H₂(D1,j) by A227, INTEGRA1:def 20;
indx (D2,D1,j1) in Seg (len D2) by A48, 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 20;
then H₂(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) = Sum ((H₁(D2) | (indx (D2,D1,j1))) ^ (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) by RVSUM_1:75
.= Sum ((mid (H₁(D2),1,(indx (D2,D1,j1)))) ^ (mid (H₁(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) by A50, FINSEQ_6:116
.= Sum (mid (H₁(D2),1,(indx (D2,D1,j)))) by A50, A52, A226, INTEGRA2:4
.= Sum (H₁(D2) | (indx (D2,D1,j))) by A133, FINSEQ_6:116 ;
then A230: H₂(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) = H₂(D2, indx (D2,D1,j)) by A225, INTEGRA1:def 20;
indx (D2,D1,j1) in Seg (len D2) by A48, FINSEQ_1:def 3;
then indx (D2,D1,j1) in Seg (len (lower_volume (f,D2))) by INTEGRA1:def 7;
then indx (D2,D1,j1) in dom (lower_volume (f,D2)) by FINSEQ_1:def 3;
then H₂(D2, indx (D2,D1,j1)) = Sum ((lower_volume (f,D2)) | (indx (D2,D1,j1))) by INTEGRA1:def 20
.= H₂(D1,j1) by A222, A46, INTEGRA1:def 20 ;
hence H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A54, A230, A229; :: thesis:

end;

hence S₁[1] by A42, A43; :: thesis:

end;

reconsider i = i as non zero Element of NAT by A18, FINSEQ_1:1;
A231: for i being non zero Nat st S₁[i] holds
S₁[i + 1]

proof

let i be non zero Nat; :: thesis:
A232: i >= 1 by NAT_1:14;
assume A233: S₁[i] ; :: thesis:
S₁[i + 1]

proof

A234: i <= i + 1 by NAT_1:11;
assume A235: i + 1 in dom D ; :: thesis:
then consider j being Element of NAT such that
A236: j in dom D1 and
A237: D . (i + 1) in divset (D1,j) by Th3, INTEGRA1:6;
A238: D2 . (indx (D2,D1,j)) = D1 . j by A13, A236, INTEGRA1:def 19;
i + 1 <= len D by A235, FINSEQ_3:25;
then i <= len D by A234, XXREAL_0:2;
then A239: i in Seg (len D) by A232, FINSEQ_1:1;
then A240: i in dom D by FINSEQ_1:def 3;
consider n1 being Element of NAT such that
A241: n1 in dom D1 and
A242: D . i in divset (D1,n1) and
A243: H₂(D2, indx (D2,D1,n1)) - H₂(D1,n1) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A233, A239, FINSEQ_1:def 3;
A244: 1 <= n1 + 1 by NAT_1:12;
A245: n1 < j

proof

assume A246: n1 >= j ; :: thesis:

now :: thesis:

per cases by A246, XXREAL_0:1;

suppose A247: n1 = j ; :: thesis:

D . i in rng D by A240, FUNCT_1:def 3;
then A248: D . i in (rng D) /\ (divset (D1,j)) by A242, A247, XBOOLE_0:def 4;
D . (i + 1) in rng D by A235, FUNCT_1:def 3;
then A249: D . (i + 1) in (rng D) /\ (divset (D1,j)) by A237, XBOOLE_0:def 4;
i + 1 > i by XREAL_1:29;
hence contradiction by A11, A235, A236, A240, A248, A249, Th5, SEQ_4:138; :: thesis:

end;

suppose n1 > j ; :: thesis:

then A250: n1 >= j + 1 by NAT_1:13;
then A251: n1 - 1 >= j by XREAL_1:19;
1 <= j by A236, FINSEQ_3:25;
then 1 + 1 <= j + 1 by XREAL_1:6;
then A252: n1 <> 1 by A250, XXREAL_0:2;
lower_bound (divset (D1,n1)) <= D . i by A242, INTEGRA2:1;
then A253: D . i >= D1 . (n1 - 1) by A241, A252, INTEGRA1:def 4;
n1 - 1 in dom D1 by A241, A252, INTEGRA1:7;
then D1 . j <= D1 . (n1 - 1) by A236, A251, SEQ_4:137;
then A254: D . i >= D1 . j by A253, XXREAL_0:2;
A255: i < i + 1 by XREAL_1:29;
A256: upper_bound (divset (D1,j)) = D1 . j

proof

per cases ;

suppose j = 1 ; :: thesis:

hence upper_bound (divset (D1,j)) = D1 . j by A236, INTEGRA1:def 4; :: thesis:

end;

suppose j <> 1 ; :: thesis:

hence upper_bound (divset (D1,j)) = D1 . j by A236, INTEGRA1:def 4; :: thesis:

end;

D . (i + 1) <= upper_bound (divset (D1,j)) by A237, INTEGRA2:1;
then D . i >= D . (i + 1) by A256, A254, XXREAL_0:2;
hence contradiction by A235, A240, A255, SEQM_3:def 1; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A257: n1 + 1 <= j by NAT_1:13;
A258: 1 <= n1 by A241, FINSEQ_3:25;
A259: indx (D2,D1,n1) in dom D2 by A13, A241, INTEGRA1:def 19;
then A260: 1 <= indx (D2,D1,n1) by FINSEQ_3:25;
A261: indx (D2,D1,j) in dom D2 by A13, A236, INTEGRA1:def 19;
then A262: 1 <= indx (D2,D1,j) by FINSEQ_3:25;
A263: indx (D2,D1,j) <= len D2 by A261, FINSEQ_3:25;
then A264: indx (D2,D1,j) <= len H₁(D2) by INTEGRA1:def 7;
A265: 1 <= j by A236, FINSEQ_3:25;
A266: j <= len D1 by A236, FINSEQ_3:25;
then A267: n1 + 1 <= len D1 by A257, XXREAL_0:2;
then A268: n1 + 1 in dom D1 by A244, FINSEQ_3:25;
then A269: indx (D2,D1,(n1 + 1)) in dom D2 by A13, INTEGRA1:def 19;
then A270: 1 <= indx (D2,D1,(n1 + 1)) by FINSEQ_3:25;
A271: D2 . (indx (D2,D1,(n1 + 1))) = D1 . (n1 + 1) by A13, A268, INTEGRA1:def 19;
then D2 . (indx (D2,D1,(n1 + 1))) <= D2 . (indx (D2,D1,j)) by A236, A257, A268, A238, SEQ_4:137;
then A272: indx (D2,D1,(n1 + 1)) <= indx (D2,D1,j) by A269, A261, SEQM_3:def 1;
then 1 + (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) + 1 by XREAL_1:6;
then 1 <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;
then A273: (mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j)))) . 1 = D2 . ((1 - 1) + (indx (D2,D1,(n1 + 1)))) by A272, A270, A263, FINSEQ_6:122
.= D1 . (n1 + 1) by A13, A268, INTEGRA1:def 19 ;
A274: D2 . (indx (D2,D1,n1)) = D1 . n1 by A13, A241, INTEGRA1:def 19;
A275: j <= len H₁(D1) by A266, INTEGRA1:def 7;
then j in Seg (len H₁(D1)) by A265, FINSEQ_1:1;
then A276: j in dom H₁(D1) by FINSEQ_1:def 3;
A277: indx (D2,D1,(n1 + 1)) <= len D2 by A269, FINSEQ_3:25;
n1 in Seg (len D1) by A241, FINSEQ_1:def 3;
then n1 in Seg (len H₁(D1)) by INTEGRA1:def 7;
then n1 in dom H₁(D1) by FINSEQ_1:def 3;
then H₂(D1,n1) = Sum (H₁(D1) | n1) by INTEGRA1:def 20
.= Sum (mid (H₁(D1),1,n1)) by A258, FINSEQ_6:116 ;
then H₂(D1,n1) + (Sum (mid (H₁(D1),(n1 + 1),j))) = Sum ((mid (H₁(D1),1,n1)) ^ (mid (H₁(D1),(n1 + 1),j))) by RVSUM_1:75
.= Sum (mid (H₁(D1),1,j)) by A245, A258, A275, INTEGRA2:4
.= Sum (H₁(D1) | j) by A265, FINSEQ_6:116 ;
then A278: H₂(D1,j) = H₂(D1,n1) + (Sum (mid (H₁(D1),(n1 + 1),j))) by A276, INTEGRA1:def 20;
indx (D2,D1,j) in Seg (len D2) by A261, FINSEQ_1:def 3;
then indx (D2,D1,j) in Seg (len H₁(D2)) by INTEGRA1:def 7;
then A279: indx (D2,D1,j) in dom H₁(D2) by FINSEQ_1:def 3;
A280: n1 >= 1 by A241, FINSEQ_3:25;
A281: j - n1 >= 1 by A257, XREAL_1:19;
(Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof

now :: thesis:

per cases by A257, XXREAL_0:1;

suppose A282: n1 + 1 = j ; :: thesis:

A283: (indx (D2,D1,j)) - (indx (D2,D1,n1)) <= 2

proof

A284: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;
A285: lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;
A286: 1 <= (indx (D2,D1,n1)) + 1 by A260, NAT_1:13;
assume (indx (D2,D1,j)) - (indx (D2,D1,n1)) > 2 ; :: thesis:
then A287: (indx (D2,D1,n1)) + 2 < indx (D2,D1,j) by XREAL_1:20;
then A288: (indx (D2,D1,n1)) + 2 <= len D2 by A263, XXREAL_0:2;
A289: (indx (D2,D1,n1)) + 1 < (indx (D2,D1,n1)) + 2 by XREAL_1:6;
then A290: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 2 by NAT_1:13;
then 1 <= (indx (D2,D1,n1)) + 2 by A260, XXREAL_0:2;
then A291: (indx (D2,D1,n1)) + 2 in dom D2 by A288, FINSEQ_3:25;
then A292: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 2) by A261, A287, SEQ_4:137;
A293: not D2 . ((indx (D2,D1,n1)) + 2) in rng D1

proof

assume D2 . ((indx (D2,D1,n1)) + 2) in rng D1 ; :: thesis:
then consider k1 being Element of NAT such that
A294: k1 in dom D1 and
A295: D2 . ((indx (D2,D1,n1)) + 2) = D1 . k1 by PARTFUN1:3;
D2 . ((indx (D2,D1,n1)) + 2) < D2 . (indx (D2,D1,j)) by A261, A287, A291, SEQM_3:def 1;
then A296: k1 < j by A236, A238, A294, A295, SEQ_4:137;
D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 2) by A259, A290, A291, SEQM_3:def 1;
then n1 < k1 by A241, A274, A294, A295, SEQ_4:137;
hence contradiction by A282, A296, NAT_1:13; :: thesis:

end;

D2 . ((indx (D2,D1,n1)) + 2) in rng D2 by A291, FUNCT_1:def 3;
then A297: D2 . ((indx (D2,D1,n1)) + 2) in rng D by A14, A293, XBOOLE_0:def 3;
A298: lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;
A299: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;
D2 . ((indx (D2,D1,n1)) + 2) >= D2 . (indx (D2,D1,n1)) by A259, A290, A291, SEQ_4:137;
then D2 . ((indx (D2,D1,n1)) + 2) in divset (D1,j) by A274, A238, A282, A298, A284, A292, INTEGRA2:1;
then A300: D2 . ((indx (D2,D1,n1)) + 2) in (rng D) /\ (divset (D1,j)) by A297, XBOOLE_0:def 4;
A301: (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) by A287, A289, XXREAL_0:2;
then (indx (D2,D1,n1)) + 1 <= len D2 by A263, XXREAL_0:2;
then A302: (indx (D2,D1,n1)) + 1 in dom D2 by A286, FINSEQ_3:25;
then A303: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 1) by A261, A301, SEQ_4:137;
A304: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;
A305: not D2 . ((indx (D2,D1,n1)) + 1) in rng D1

proof

assume D2 . ((indx (D2,D1,n1)) + 1) in rng D1 ; :: thesis:
then consider k1 being Element of NAT such that
A306: k1 in dom D1 and
A307: D2 . ((indx (D2,D1,n1)) + 1) = D1 . k1 by PARTFUN1:3;
D2 . ((indx (D2,D1,n1)) + 1) < D2 . (indx (D2,D1,j)) by A261, A301, A302, SEQM_3:def 1;
then A308: k1 < j by A236, A238, A306, A307, SEQ_4:137;
D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A259, A304, A302, SEQM_3:def 1;
then n1 < k1 by A241, A274, A306, A307, SEQ_4:137;
hence contradiction by A282, A308, NAT_1:13; :: thesis:

end;

D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by A302, FUNCT_1:def 3;
then A309: D2 . ((indx (D2,D1,n1)) + 1) in rng D by A14, A305, XBOOLE_0:def 3;
D2 . ((indx (D2,D1,n1)) + 1) >= D2 . (indx (D2,D1,n1)) by A259, A304, A302, SEQ_4:137;
then D2 . ((indx (D2,D1,n1)) + 1) in divset (D1,j) by A274, A238, A282, A285, A299, A303, INTEGRA2:1;
then D2 . ((indx (D2,D1,n1)) + 1) in (rng D) /\ (divset (D1,j)) by A309, XBOOLE_0:def 4;
then D2 . ((indx (D2,D1,n1)) + 1) = D2 . ((indx (D2,D1,n1)) + 2) by A11, A236, A300, Th5;
hence contradiction by A289, A302, A291, SEQM_3:def 1; :: thesis:

end;

A310: ( (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) implies (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) )

proof

assume (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ; :: thesis:
then A311: ((indx (D2,D1,n1)) + 1) + 1 <= indx (D2,D1,j) by NAT_1:13;
(indx (D2,D1,n1)) + 2 >= indx (D2,D1,j) by A283, XREAL_1:20;
hence (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) by A311, XXREAL_0:1; :: thesis:

end;

A312: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;
A313: indx (D2,D1,j) <= len H₁(D2) by A263, INTEGRA1:def 7;
D1 . n1 < D1 . j by A236, A241, A245, SEQM_3:def 1;
then A314: indx (D2,D1,n1) < indx (D2,D1,j) by A259, A274, A261, A238, SEQ_4:137;
then A315: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by NAT_1:13;
then (indx (D2,D1,n1)) + 1 <= len D2 by A263, XXREAL_0:2;
then (indx (D2,D1,n1)) + 1 <= len H₁(D2) by INTEGRA1:def 7;
then A316: len (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) = ((indx (D2,D1,j)) -' ((indx (D2,D1,n1)) + 1)) + 1 by A262, A315, A312, A313, FINSEQ_6:118
.= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A315, XREAL_1:233
.= (indx (D2,D1,j)) - (indx (D2,D1,n1)) ;
(indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A314, NAT_1:13;
then A317: ( (indx (D2,D1,n1)) + 1 = indx (D2,D1,j) or (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ) by XXREAL_0:1;
A318: Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))

proof

per cases ) - (indx (D2,D1,n1)) = 1 or (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2 ) by A317, A310;

suppose A319: (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1 ; :: thesis:

A320: (indx (D2,D1,n1)) + 1 > 1 by A260, NAT_1:13;
then upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A261, A319, INTEGRA1:def 4;
then A321: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . j by A13, A236, A319, INTEGRA1:def 19;
lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A261, A319, A320, INTEGRA1:def 4;
then A322: lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . n1 by A13, A241, INTEGRA1:def 19;
lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A280, A268, A282, INTEGRA1:def 4;
then A323: divset (D2,((indx (D2,D1,n1)) + 1)) = divset (D1,(n1 + 1)) by A245, A280, A268, A282, A322, A321, INTEGRA1:def 4;
A324: vol (divset (D2,((indx (D2,D1,n1)) + 1))) >= 0 by INTEGRA1:9;
reconsider LV = H₁(D2) . ((indx (D2,D1,n1)) + 1) as Element of REAL by XREAL_0:def 1;
1 = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A319;
then (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 1 = H₁(D2) . ((1 + ((indx (D2,D1,n1)) + 1)) - 1) by A312, A313, FINSEQ_6:122
.= H₁(D2) . ((indx (D2,D1,n1)) + 1) ;
then A325: mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*LV*> by A316, A319, FINSEQ_1:40;
H₁(D2) . ((indx (D2,D1,n1)) + 1) = (lower_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 1)))) by A261, A319, INTEGRA1:def 7;
then H₁(D2) . ((indx (D2,D1,n1)) + 1) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1)))) by A1, A261, A319, A323, A324, Th18, XREAL_1:64;
hence Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1)))) by A325, FINSOP_1:11; :: thesis:

end;

suppose A326: (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2 ; :: thesis:

(indx (D2,D1,n1)) + 2 >= 2 + 1 by A260, XREAL_1:6;
then A327: (indx (D2,D1,n1)) + 2 <> 1 ;
then A328: upper_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . (indx (D2,D1,j)) by A261, A326, INTEGRA1:def 4;
((indx (D2,D1,n1)) + 2) - 1 = (indx (D2,D1,n1)) + 1 ;
then lower_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . ((indx (D2,D1,n1)) + 1) by A261, A326, A327, INTEGRA1:def 4;
then A329: vol (divset (D2,((indx (D2,D1,n1)) + 2))) = (D1 . j) - (D2 . ((indx (D2,D1,n1)) + 1)) by A238, A328, INTEGRA1:def 5;
A330: upper_bound (divset (D1,(n1 + 1))) = D1 . (n1 + 1) by A245, A280, A268, A282, INTEGRA1:def 4;
lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A280, A268, A282, INTEGRA1:def 4;
then A331: vol (divset (D1,(n1 + 1))) = (D1 . (n1 + 1)) - (D1 . n1) by A330, INTEGRA1:def 5;
A332: vol (divset (D2,((indx (D2,D1,n1)) + 2))) >= 0 by INTEGRA1:9;
A333: indx (D2,D1,j) <= len H₁(D2) by A263, INTEGRA1:def 7;
A334: vol (divset (D2,((indx (D2,D1,n1)) + 1))) >= 0 by INTEGRA1:9;
A335: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;
A336: (indx (D2,D1,n1)) + 1 <= (indx (D2,D1,n1)) + 2 by XREAL_1:6;
then (indx (D2,D1,n1)) + 1 <= len D2 by A263, A326, XXREAL_0:2;
then A337: (indx (D2,D1,n1)) + 1 in dom D2 by A335, FINSEQ_3:25;
then H₁(D2) . ((indx (D2,D1,n1)) + 1) = (lower_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 1)))) by INTEGRA1:def 7;
then A338: H₁(D2) . ((indx (D2,D1,n1)) + 1) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 1)))) by A1, A337, A334, Th18, XREAL_1:64;
((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 = 1 + 1 by A326;
then A339: (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 2 = H₁(D2) . ((2 + ((indx (D2,D1,n1)) + 1)) - 1) by A335, A336, A333, FINSEQ_6:122
.= H₁(D2) . (((indx (D2,D1,n1)) + 0) + 2) ;
((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 >= 1 by A326;
then (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 1 = H₁(D2) . ((1 + ((indx (D2,D1,n1)) + 1)) - 1) by A326, A335, A336, A333, FINSEQ_6:122
.= H₁(D2) . ((indx (D2,D1,n1)) + 1) ;
then mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*(H₁(D2) . ((indx (D2,D1,n1)) + 1)),(H₁(D2) . ((indx (D2,D1,n1)) + 2))*> by A316, A326, A339, FINSEQ_1:44;
then A340: Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) = (H₁(D2) . ((indx (D2,D1,n1)) + 1)) + (H₁(D2) . ((indx (D2,D1,n1)) + 2)) by RVSUM_1:77;
A341: (indx (D2,D1,n1)) + 1 > 1 by A260, NAT_1:13;
then A342: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A337, INTEGRA1:def 4;
lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A337, A341, INTEGRA1:def 4;
then A343: vol (divset (D2,((indx (D2,D1,n1)) + 1))) = (D2 . ((indx (D2,D1,n1)) + 1)) - (D1 . n1) by A274, A342, INTEGRA1:def 5;
H₁(D2) . ((indx (D2,D1,n1)) + 2) = (lower_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 2)))) by A261, A326, INTEGRA1:def 7;
then H₁(D2) . ((indx (D2,D1,n1)) + 2) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 2)))) by A1, A261, A326, A332, Th18, XREAL_1:64;
then Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))) + ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 2))))) by A340, A338, XREAL_1:7;
hence Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1)))) by A282, A343, A329, A331; :: thesis:

end;

A344: n1 + 1 <= len H₁(D1) by A267, INTEGRA1:def 7;
then A345: len (mid (H₁(D1),(n1 + 1),j)) = (j -' (n1 + 1)) + 1 by A244, A282, FINSEQ_6:118
.= (j - j) + 1 by A282, XREAL_1:233
.= 1 ;
reconsider lv = (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) as Element of REAL by XREAL_0:def 1;
(n1 + 1) + 1 <= j + 1 by A257, XREAL_1:6;
then 1 <= (j + 1) - (n1 + 1) by XREAL_1:19;
then (mid (H₁(D1),(n1 + 1),j)) . 1 = H₁(D1) . ((1 - 1) + (n1 + 1)) by A244, A282, A344, FINSEQ_6:122
.= (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) by A268, INTEGRA1:def 7 ;
then mid (H₁(D1),(n1 + 1),j) = <*lv*> by A345, FINSEQ_1:40;
then A346: Sum (mid (H₁(D1),(n1 + 1),j)) = (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) by FINSOP_1:11;
divset (D1,(n1 + 1)) c= A by A268, INTEGRA1:8;
then A347: lower_bound (rng (f | (divset (D1,(n1 + 1))))) >= lower_bound (rng f) by A1, Lm4;
n1 + 1 in Seg (len D1) by A268, FINSEQ_1:def 3;
then n1 + 1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;
then A348: n1 + 1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;
vol (divset (D1,(n1 + 1))) = (upper_volume ((chi (A,A)),D1)) . (n1 + 1) by A268, INTEGRA1:20;
then vol (divset (D1,(n1 + 1))) in rng (upper_volume ((chi (A,A)),D1)) by A348, FUNCT_1:def 3;
then A349: vol (divset (D1,(n1 + 1))) <= delta D1 by XXREAL_2:def 8;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
then A350: ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,(n1 + 1)))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A349, XREAL_1:64;
vol (divset (D1,(n1 + 1))) >= 0 by INTEGRA1:9;
then Sum (mid (H₁(D1),(n1 + 1),j)) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1)))) by A346, A347, XREAL_1:64;
then (Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))) - ((lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))) by A318, XREAL_1:13;
hence (Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A350, XXREAL_0:2; :: thesis:

end;

suppose A351: n1 + 1 < j ; :: thesis:

A352: n1 < n1 + 1 by NAT_1:13;
then A353: D1 . n1 < D1 . (n1 + 1) by A241, A268, SEQM_3:def 1;
then consider B being non empty closed_interval Subset of REAL, MD1, MD2 being Division of B such that
A354: D1 . n1 = lower_bound B and
upper_bound B = MD2 . (len MD2) and
A355: upper_bound B = MD1 . (len MD1) and
A356: MD1 <= MD2 and
A357: MD1 = mid (D1,(n1 + 1),j) and
A358: MD2 = mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j))) by A13, A236, A257, A268, A273, Th15;
A359: delta MD1 >= 0 by Th9;
A360: len MD1 = (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;
then A361: ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A257, XREAL_1:233
.= j ;
j -' (n1 + 1) = j - (n1 + 1) by A257, XREAL_1:233;
then A362: (j -' (n1 + 1)) + 1 = j - n1 ;
then A363: len MD1 = j - n1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;
A364: B c= A

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis:
A365: rng D1 c= A by INTEGRA1:def 2;
D1 . n1 in rng D1 by A241, FUNCT_1:def 3;
then A366: lower_bound A <= D1 . n1 by A365, INTEGRA2:1;
assume A367: x1 in B ; :: thesis:
then reconsider x1 = x1 as Real ;
A368: x1 <= MD1 . (len MD1) by A355, A367, INTEGRA2:1;
D1 . j in rng D1 by A236, FUNCT_1:def 3;
then A369: D1 . j <= upper_bound A by A365, INTEGRA2:1;
D1 . n1 <= x1 by A354, A367, INTEGRA2:1;
then A370: lower_bound A <= x1 by A366, XXREAL_0:2;
MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A257, A281, A266, A244, A357, A362, A363, FINSEQ_6:122
.= D1 . j ;
then x1 <= upper_bound A by A368, A369, XXREAL_0:2;
hence x1 in A by A370, INTEGRA2:1; :: thesis:

end;

then reconsider g = f | B as Function of B,REAL by FUNCT_2:32;
A371: len (lower_volume (g,MD1)) = len MD1 by INTEGRA1:def 7
.= (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118
.= (j - (n1 + 1)) + 1 by A257, XREAL_1:233 ;
A372: len MD1 in dom MD1 by FINSEQ_5:6;
then A373: 1 <= len MD1 by FINSEQ_3:25;
A374: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

proof

per cases ;

suppose A375: len MD1 = 1 ; :: thesis:

then A376: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A372, INTEGRA1:def 4;
A377: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;
lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;
hence ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) ) by A265, A266, A354, A357, A361, A372, A375, A376, A377, FINSEQ_6:118, INTEGRA1:def 4; :: thesis:

end;

suppose A378: len MD1 <> 1 ; :: thesis:

then (len MD1) - 1 in dom MD1 by A372, INTEGRA1:7;
then A379: (len MD1) - 1 >= 1 by FINSEQ_3:25;
len MD1 <= (len MD1) + 1 by NAT_1:11;
then A380: (len MD1) - 1 <= len MD1 by XREAL_1:20;
upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A372, A378, INTEGRA1:def 4;
then A381: upper_bound (divset (MD1,(len MD1))) = D1 . j by A257, A266, A244, A357, A360, A361, A373, FINSEQ_6:122;
A382: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A363;
lower_bound (divset (MD1,(len MD1))) = MD1 . ((len MD1) - 1) by A372, A378, INTEGRA1:def 4;
then lower_bound (divset (MD1,(len MD1))) = D1 . (j - 1) by A257, A266, A244, A357, A360, A382, A379, A380, FINSEQ_6:122;
hence ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) ) by A236, A245, A280, A381, INTEGRA1:def 4; :: thesis:

end;

A383: len MD1 in dom MD1 by FINSEQ_5:6;
A384: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

proof

per cases ;

suppose len MD1 = 1 ; :: thesis:

hence upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A383, INTEGRA1:def 4; :: thesis:

end;

suppose len MD1 <> 1 ; :: thesis:

hence upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A383, INTEGRA1:def 4; :: thesis:

end;

D1 . n1 < D1 . (n1 + 1) by A241, A268, A352, SEQM_3:def 1;
then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A259, A274, A269, A271, SEQ_4:137;
then A385: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,(n1 + 1)) by NAT_1:13;
then A386: (indx (D2,D1,n1)) + 1 <= len D2 by A277, XXREAL_0:2;
vol B = (upper_bound B) - (D1 . n1) by A354, INTEGRA1:def 5;
then vol B = (D1 . j) - (D1 . n1) by A236, A245, A280, A355, A374, A384, INTEGRA1:def 4;
then A387: vol B <> 0 by A236, A241, A245, SEQM_3:def 1;
A388: 1 <= (indx (D2,D1,n1)) + 1 by A260, NAT_1:13;
A389: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;
A390: indx (D2,D1,(n1 + 1)) = (indx (D2,D1,n1)) + 1

proof

assume indx (D2,D1,(n1 + 1)) <> (indx (D2,D1,n1)) + 1 ; :: thesis:
then A391: indx (D2,D1,(n1 + 1)) > (indx (D2,D1,n1)) + 1 by A385, XXREAL_0:1;
A392: (indx (D2,D1,n1)) + 1 in dom D2 by A388, A386, FINSEQ_3:25;
then A393: D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by FUNCT_1:def 3;

now :: thesis:

per cases by A14, A393, XBOOLE_0:def 3;

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

then consider n2 being Element of NAT such that
A394: n2 in dom D1 and
A395: D2 . ((indx (D2,D1,n1)) + 1) = D1 . n2 by PARTFUN1:3;
D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A259, A389, A392, SEQM_3:def 1;
then n1 < n2 by A241, A274, A394, A395, SEQ_4:137;
then A396: n1 + 1 <= n2 by NAT_1:13;
D1 . n2 < D1 . (n1 + 1) by A269, A271, A391, A392, A395, SEQM_3:def 1;
hence contradiction by A268, A394, A396, SEQ_4:137; :: thesis:

end;

suppose A397: D2 . ((indx (D2,D1,n1)) + 1) in rng D ; :: thesis:

A398: D . i <= upper_bound (divset (D1,n1)) by A242, INTEGRA2:1;
A399: upper_bound (divset (D1,n1)) = D1 . n1

proof

per cases ;

suppose n1 = 1 ; :: thesis:

hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis:

end;

suppose n1 <> 1 ; :: thesis:

hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis:

end;

consider n2 being Element of NAT such that
A400: n2 in dom D and
A401: D2 . ((indx (D2,D1,n1)) + 1) = D . n2 by A397, PARTFUN1:3;
D1 . n1 < D . n2 by A259, A274, A389, A392, A401, SEQM_3:def 1;
then D . i < D . n2 by A398, A399, XXREAL_0:2;
then i < n2 by A240, A400, SEQ_4:137;
then A402: i + 1 <= n2 by NAT_1:13;
(n1 + 1) + 1 <= j by A351, NAT_1:13;
then A403: n1 + 1 <= j - 1 by XREAL_1:19;
j - 1 in dom D1 by A236, A245, A280, INTEGRA1:7;
then A404: D1 . (n1 + 1) <= D1 . (j - 1) by A268, A403, SEQ_4:137;
A405: lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;
lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;
then A406: D1 . (n1 + 1) <= D . (i + 1) by A404, A405, XXREAL_0:2;
D . n2 < D1 . (n1 + 1) by A269, A271, A391, A392, A401, SEQM_3:def 1;
then D . n2 < D . (i + 1) by A406, XXREAL_0:2;
hence contradiction by A235, A400, A402, SEQ_4:137; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A407: j <= len H₁(D1) by A266, INTEGRA1:def 7;
A408: for k being Nat st 1 <= k & k <= len (lower_volume (g,MD1)) holds
(lower_volume (g,MD1)) . k = (mid (H₁(D1),(n1 + 1),j)) . k

proof

let k be Nat; :: thesis:
assume that
A409: 1 <= k and
A410: k <= len (lower_volume (g,MD1)) ; :: thesis:
k in Seg (len (lower_volume (g,MD1))) by A409, A410, FINSEQ_1:1;
then A411: k in Seg (len MD1) by INTEGRA1:def 7;
then A412: k in dom MD1 by FINSEQ_1:def 3;
k in dom MD1 by A411, FINSEQ_1:def 3;
then A413: (lower_volume (g,MD1)) . k = (lower_bound (rng (g | (divset (MD1,k))))) * (vol (divset (MD1,k))) by INTEGRA1:def 7;
consider k2 being Element of NAT such that
A414: n1 + 1 = 1 + k2 ;
A415: 1 <= k + k2 by A409, NAT_1:12;
k <= j - ((n1 + 1) - 1) by A371, A410;
then k + ((n1 + 1) - 1) <= j by XREAL_1:19;
then k + k2 <= len D1 by A266, A414, XXREAL_0:2;
then A416: k + k2 in Seg (len D1) by A415, FINSEQ_1:1;
then A417: k + k2 in dom D1 by FINSEQ_1:def 3;
1 + 1 <= k + k2 by A258, A409, A414, XREAL_1:7;
then A418: 1 < k + k2 by NAT_1:13;
A419: k2 = (n1 + 1) - 1 by A414;
A420: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )

proof

per cases ;

suppose A421: k = 1 ; :: thesis:

then upper_bound (divset (MD1,k)) = MD1 . k by A412, INTEGRA1:def 4;
then A422: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A371, A409, A410, FINSEQ_6:122;
lower_bound (divset (MD1,k)) = D1 . n1 by A354, A412, A421, INTEGRA1:def 4;
hence ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) ) by A419, A418, A417, A421, A422, INTEGRA1:def 4; :: thesis:

end;

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

then upper_bound (divset (MD1,k)) = MD1 . k by A412, INTEGRA1:def 4;
then A424: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A371, A409, A410, FINSEQ_6:122;
A425: k - 1 <= (j - (n1 + 1)) + 1 by A371, A410, XREAL_1:146, XXREAL_0:2;
A426: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A412, A423, INTEGRA1:def 4;
A427: k - 1 in dom MD1 by A412, A423, INTEGRA1:7;
then 1 <= k - 1 by FINSEQ_3:25;
then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A257, A266, A244, A357, A427, A425, A426, FINSEQ_6:122;
hence ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) ) by A414, A418, A417, A424, INTEGRA1:def 4; :: thesis:

end;

divset (MD1,k) = [.(lower_bound (divset (MD1,k))),(upper_bound (divset (MD1,k))).] by INTEGRA1:4;
then A428: divset (D1,(k + k2)) = divset (MD1,k) by A420, INTEGRA1:4;
A429: k + k2 in dom D1 by A416, FINSEQ_1:def 3;
A430: (mid (H₁(D1),(n1 + 1),j)) . k = H₁(D1) . ((k + (n1 + 1)) - 1) by A257, A244, A371, A407, A409, A410, FINSEQ_6:122
.= (lower_bound (rng (f | (divset (D1,(k + k2)))))) * (vol (divset (D1,(k + k2)))) by A414, A429, INTEGRA1:def 7 ;
k in dom MD1 by A411, FINSEQ_1:def 3;
then divset (D1,(k + k2)) c= B by A428, INTEGRA1:8;
hence (lower_volume (g,MD1)) . k = (mid (H₁(D1),(n1 + 1),j)) . k by A413, A430, A428, FUNCT_1:51; :: thesis:

end;

A431: g | B is bounded

proof

consider a being Real such that
A432: for x being object st x in A /\ (dom f) holds
a <= f . x by A1, RFUNCT_1:71;
for x being object st x in B /\ (dom g) holds
a <= g . x

proof

let x be object ; :: thesis:
A433: (dom f) /\ B c= (dom f) /\ A by A364, XBOOLE_1:26;
assume x in B /\ (dom g) ; :: thesis:
then A434: x in dom g by XBOOLE_0:def 4;
then x in (dom f) /\ B by RELAT_1:61;
then a <= f . x by A432, A433;
hence a <= g . x by A434, FUNCT_1:47; :: thesis:

end;

then A435: g | B is bounded_below by RFUNCT_1:71;
consider a being Real such that
A436: for x being object st x in A /\ (dom f) holds
f . x <= a by A1, RFUNCT_1:70;
for x being object st x in B /\ (dom g) holds
g . x <= a

proof

let x be object ; :: thesis:
A437: (dom f) /\ B c= (dom f) /\ A by A364, XBOOLE_1:26;
assume x in B /\ (dom g) ; :: thesis:
then A438: x in dom g by XBOOLE_0:def 4;
then x in (dom f) /\ B by RELAT_1:61;
then a >= f . x by A436, A437;
hence g . x <= a by A438, FUNCT_1:47; :: thesis:

end;

then g | B is bounded_above by RFUNCT_1:70;
hence g | B is bounded by A435; :: thesis:

end;

rng f is bounded_below by A1, INTEGRA1:11;
then A439: lower_bound (rng f) <= lower_bound (rng g) by RELAT_1:70, SEQ_4:47;
rng f is bounded_above by A1, INTEGRA1:13;
then upper_bound (rng f) >= upper_bound (rng g) by RELAT_1:70, SEQ_4:48;
then (upper_bound (rng f)) - (lower_bound (rng f)) >= (upper_bound (rng g)) - (lower_bound (rng g)) by A439, XREAL_1:13;
then A440: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A359, XREAL_1:64;
A441: n1 < j - 1 by A351, XREAL_1:20;
A442: indx (D2,D1,j) <= len H₁(D2) by A263, INTEGRA1:def 7;
A443: len MD2 = ((indx (D2,D1,j)) -' (indx (D2,D1,(n1 + 1)))) + 1 by A272, A270, A277, A262, A263, A358, FINSEQ_6:118;
then A444: len MD2 = ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by A272, XREAL_1:233;
then A445: len (lower_volume (g,MD2)) = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A390, INTEGRA1:def 7;
for x1 being object st x1 in (rng MD1) \/ {(D . (i + 1))} holds
x1 in rng MD2

proof

let x1 be object ; :: thesis:
assume A446: x1 in (rng MD1) \/ {(D . (i + 1))} ; :: thesis:
then reconsider x1 = x1 as Real ;

now :: thesis:

per cases by A446, XBOOLE_0:def 3;

suppose A447: x1 in rng MD1 ; :: thesis:

rng MD1 <> {} ;
then 1 in dom MD1 by FINSEQ_3:32;
then A448: 1 <= len MD1 by FINSEQ_3:25;
rng MD1 c= rng D1 by A357, FINSEQ_6:119;
then A449: x1 in rng D1 by A447;
rng D1 c= rng D2 by A13, INTEGRA1:def 18;
then consider k being Element of NAT such that
A450: k in dom D2 and
A451: D2 . k = x1 by A449, PARTFUN1:3;
MD1 . 1 = D1 . (n1 + 1) by A265, A266, A244, A267, A357, FINSEQ_6:118;
then D2 . (indx (D2,D1,(n1 + 1))) <= x1 by A271, A447, Th16;
then A452: indx (D2,D1,(n1 + 1)) <= k by A269, A450, A451, SEQM_3:def 1;
then consider n being Nat such that
A453: k + 1 = (indx (D2,D1,(n1 + 1))) + n by NAT_1:10, NAT_1:12;
A454: len MD1 = (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;
then ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A257, XREAL_1:233
.= j ;
then MD1 . (len MD1) = D1 . j by A257, A266, A244, A357, A448, A454, FINSEQ_6:122;
then x1 <= D2 . (indx (D2,D1,j)) by A238, A447, Th16;
then k <= indx (D2,D1,j) by A261, A450, A451, SEQM_3:def 1;
then k - (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1))) by XREAL_1:9;
then A455: (k - (indx (D2,D1,(n1 + 1)))) + 1 <= ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by XREAL_1:6;
(indx (D2,D1,(n1 + 1))) + 1 <= k + 1 by A452, XREAL_1:6;
then A456: 1 <= (k + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;
then A457: n in dom MD2 by A444, A455, A453, FINSEQ_3:25;
MD2 . n = D2 . ((n + (indx (D2,D1,(n1 + 1)))) - 1) by A272, A270, A263, A358, A456, A455, A453, FINSEQ_6:122
.= D2 . k by A453 ;
hence x1 in rng MD2 by A451, A457, FUNCT_1:def 3; :: thesis:

end;

suppose x1 in {(D . (i + 1))} ; :: thesis:

then A458: x1 = D . (i + 1) by TARSKI:def 1;
reconsider j1 = j - 1 as Element of NAT by A236, A245, A280, INTEGRA1:7;
A459: rng D c= rng D2 by A12, INTEGRA1:def 18;
D . (i + 1) in rng D by A235, FUNCT_1:def 3;
then consider k being Element of NAT such that
A460: k in dom D2 and
A461: x1 = D2 . k by A458, A459, PARTFUN1:3;
D . (i + 1) <= upper_bound (divset (D1,j)) by A237, INTEGRA2:1;
then x1 <= D1 . j by A236, A245, A280, A458, INTEGRA1:def 4;
then A462: D2 . k <= D2 . (indx (D2,D1,j)) by A13, A236, A461, INTEGRA1:def 19;
n1 < j1 by A351, XREAL_1:20;
then A463: n1 + 1 <= j1 by NAT_1:13;
j - 1 in dom D1 by A236, A245, A280, INTEGRA1:7;
then A464: D1 . (n1 + 1) <= D1 . (j - 1) by A268, A463, SEQ_4:137;
lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;
then D1 . (j - 1) <= x1 by A236, A245, A280, A458, INTEGRA1:def 4;
then D2 . (indx (D2,D1,(n1 + 1))) <= D2 . k by A271, A461, A464, XXREAL_0:2;
hence x1 in rng MD2 by A269, A261, A358, A460, A461, A462, Th17; :: thesis:

end;

hence x1 in rng MD2 ; :: thesis:

end;

then A465: (rng MD1) \/ {(D . (i + 1))} c= rng MD2 ;
rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:32;
then A466: 1 <= len MD2 by FINSEQ_3:25;
A467: ((len MD2) - 1) + (indx (D2,D1,(n1 + 1))) = indx (D2,D1,j) by A444;
for x1 being object st x1 in rng MD2 holds
x1 in (rng MD1) \/ {(D . (i + 1))}

proof

let x1 be object ; :: thesis:
assume A468: x1 in rng MD2 ; :: thesis:
then reconsider x1 = x1 as Real ;
MD2 . 1 = D2 . (indx (D2,D1,(n1 + 1))) by A270, A277, A262, A263, A358, FINSEQ_6:118;
then A469: D1 . (n1 + 1) <= x1 by A271, A468, Th16;
MD2 . (len MD2) = D2 . (indx (D2,D1,j)) by A272, A270, A263, A358, A466, A443, A467, FINSEQ_6:122;
then A470: x1 <= D1 . j by A238, A468, Th16;
A471: rng MD2 c= rng D2 by A358, FINSEQ_6:119;

now :: thesis:

per cases by A14, A468, A471, XBOOLE_0:def 3;

suppose x1 in rng D1 ; :: thesis:

then consider k being Element of NAT such that
A472: k in dom D1 and
A473: D1 . k = x1 by PARTFUN1:3;
A474: n1 + 1 <= k by A268, A469, A472, A473, SEQM_3:def 1;
then A475: 1 <= k - n1 by XREAL_1:19;
n1 <= n1 + 1 by NAT_1:11;
then consider n being Nat such that
A476: k = n1 + n by A474, NAT_1:10, XXREAL_0:2;
A477: k <= j by A236, A470, A472, A473, SEQM_3:def 1;
then k - n1 <= len MD1 by A363, XREAL_1:9;
then n in dom MD1 by A475, A476, FINSEQ_3:25;
then A478: MD1 . n in rng MD1 by FUNCT_1:def 3;
(j - (n1 + 1)) + 1 = j - n1 ;
then A479: k - n1 <= (j - (n1 + 1)) + 1 by A477, XREAL_1:9;
MD1 . n = D1 . (((k - n1) - 1) + (n1 + 1)) by A257, A266, A244, A357, A475, A479, A476, FINSEQ_6:122
.= D1 . k ;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by A473, A478, XBOOLE_0:def 3; :: thesis:

end;

suppose x1 in rng D ; :: thesis:

then consider n being Element of NAT such that
A480: n in dom D and
A481: D . n = x1 by PARTFUN1:3;
A482: not i + 1 < n

proof

A483: upper_bound (divset (D1,j)) = D1 . j

proof

per cases ;

suppose j = 1 ; :: thesis:

hence upper_bound (divset (D1,j)) = D1 . j by A236, INTEGRA1:def 4; :: thesis:

end;

suppose j <> 1 ; :: thesis:

hence upper_bound (divset (D1,j)) = D1 . j by A236, INTEGRA1:def 4; :: thesis:

end;

reconsider y1 = D . (i + 1) as Real ;
A484: D . n in rng D by A480, FUNCT_1:def 3;
assume i + 1 < n ; :: thesis:
then A485: D . (i + 1) < D . n by A235, A480, SEQM_3:def 1;
lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;
then lower_bound (divset (D1,j)) <= D . n by A485, XXREAL_0:2;
then D . n in divset (D1,j) by A470, A481, A483, INTEGRA2:1;
then A486: x1 in (rng D) /\ (divset (D1,j)) by A481, A484, XBOOLE_0:def 4;
D . (i + 1) in rng D by A235, FUNCT_1:def 3;
then y1 in (rng D) /\ (divset (D1,j)) by A237, XBOOLE_0:def 4;
hence contradiction by A11, A236, A481, A485, A486, Th5; :: thesis:

end;

A487: upper_bound (divset (D1,n1)) = D1 . n1

proof

per cases ;

suppose n1 = 1 ; :: thesis:

hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis:

end;

suppose n1 <> 1 ; :: thesis:

hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis:

end;

D . i <= upper_bound (divset (D1,n1)) by A242, INTEGRA2:1;
then D . i < D1 . (n1 + 1) by A353, A487, XXREAL_0:2;
then D . i < D . n by A469, A481, XXREAL_0:2;
then i < n by A240, A480, SEQ_4:137;
then i + 1 <= n by NAT_1:13;
then ( i + 1 = n or i + 1 < n ) by XXREAL_0:1;
then x1 in {(D . (i + 1))} by A481, A482, TARSKI:def 1;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by XBOOLE_0:def 3; :: thesis:

end;

hence x1 in (rng MD1) \/ {(D . (i + 1))} ; :: thesis:

end;

then rng MD2 c= (rng MD1) \/ {(D . (i + 1))} ;
then A488: rng MD2 = (rng MD1) \/ {(D . (i + 1))} by A465, XBOOLE_0:def 10;
delta MD1 in rng (upper_volume ((chi (B,B)),MD1)) by XXREAL_2:def 8;
then consider k being Element of NAT such that
A489: k in dom (upper_volume ((chi (B,B)),MD1)) and
A490: (upper_volume ((chi (B,B)),MD1)) . k = delta MD1 by PARTFUN1:3;
A491: k in Seg (len (upper_volume ((chi (B,B)),MD1))) by A489, FINSEQ_1:def 3;
then A492: k in Seg (len MD1) by INTEGRA1:def 6;
then A493: k in dom MD1 by FINSEQ_1:def 3;
A494: k <= len MD1 by A492, FINSEQ_1:1;
then k + n1 <= j by A363, XREAL_1:19;
then A495: k + n1 <= len D1 by A266, XXREAL_0:2;
A496: 1 <= k by A491, FINSEQ_1:1;
A497: n1 + 1 > 1 by A280, NAT_1:13;
then n1 > 1 - 1 by XREAL_1:19;
then A498: k < k + n1 by XREAL_1:29;
then 1 < k + n1 by A496, XXREAL_0:2;
then A499: k + n1 in dom D1 by A495, FINSEQ_3:25;
( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) )

proof

per cases ;

suppose A500: k = 1 ; :: thesis:

then upper_bound (divset (MD1,k)) = MD1 . k by A493, INTEGRA1:def 4;
then A501: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A360, A496, A494, FINSEQ_6:122;
lower_bound (divset (D1,(k + n1))) = D1 . ((k + n1) - 1) by A496, A498, A499, INTEGRA1:def 4;
hence ( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) ) by A354, A497, A493, A499, A500, A501, INTEGRA1:def 4; :: thesis:

end;

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

then upper_bound (divset (MD1,k)) = MD1 . k by A493, INTEGRA1:def 4;
then A503: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A360, A496, A494, FINSEQ_6:122;
A504: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A493, A502, INTEGRA1:def 4;
A505: k - 1 in dom MD1 by A493, A502, INTEGRA1:7;
then A506: k - 1 <= len MD1 by FINSEQ_3:25;
1 <= k - 1 by A505, FINSEQ_3:25;
then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A257, A266, A244, A357, A360, A505, A506, A504, FINSEQ_6:122;
hence ( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) ) by A496, A498, A499, A503, INTEGRA1:def 4; :: thesis:

end;

then divset (MD1,k) = [.(lower_bound (divset (D1,(k + n1)))),(upper_bound (divset (D1,(k + n1)))).] by INTEGRA1:4;
then A507: divset (MD1,k) = divset (D1,(k + n1)) by INTEGRA1:4;
k + n1 in Seg (len D1) by A499, FINSEQ_1:def 3;
then k + n1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;
then A508: k + n1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;
k in dom MD1 by A492, FINSEQ_1:def 3;
then delta MD1 = vol (divset (MD1,k)) by A490, INTEGRA1:20;
then delta MD1 = (upper_volume ((chi (A,A)),D1)) . (k + n1) by A499, A507, INTEGRA1:20;
then delta MD1 in rng (upper_volume ((chi (A,A)),D1)) by A508, FUNCT_1:def 3;
then delta MD1 <= max (rng (upper_volume ((chi (A,A)),D1))) by XXREAL_2:def 8;
then A509: delta MD1 <= delta D1 ;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
then A510: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A509, XREAL_1:64;
lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;
then A511: D1 . (j - 1) <= D . (i + 1) by A236, A245, A280, INTEGRA1:def 4;
A512: D . (i + 1) <= upper_bound (divset (D1,j)) by A237, INTEGRA2:1;
A513: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A272, A385, XXREAL_0:2;
A514: for k being Nat st 1 <= k & k <= len (lower_volume (g,MD2)) holds
(lower_volume (g,MD2)) . k = (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k

proof

let k be Nat; :: thesis:
assume that
A515: 1 <= k and
A516: k <= len (lower_volume (g,MD2)) ; :: thesis:
A517: k in Seg (len (lower_volume (g,MD2))) by A515, A516, FINSEQ_1:1;
A518: (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k = H₁(D2) . ((k + ((indx (D2,D1,n1)) + 1)) - 1) by A388, A445, A442, A513, A515, A516, FINSEQ_6:122;
1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;
then 1 + 1 <= k + ((indx (D2,D1,n1)) + 1) by A515, XREAL_1:7;
then A519: 1 <= (k + ((indx (D2,D1,n1)) + 1)) - 1 by XREAL_1:19;
consider k2 being Element of NAT such that
A520: (indx (D2,D1,n1)) + 1 = 1 + k2 ;
k <= (indx (D2,D1,j)) - (((indx (D2,D1,n1)) + 1) - 1) by A444, A390, A516, INTEGRA1:def 7;
then k + (((indx (D2,D1,n1)) + 1) - 1) <= indx (D2,D1,j) by XREAL_1:19;
then (k + ((indx (D2,D1,n1)) + 1)) - 1 <= len H₁(D2) by A442, XXREAL_0:2;
then k + k2 in Seg (len H₁(D2)) by A519, A520, FINSEQ_1:1;
then A521: k + k2 in Seg (len D2) by INTEGRA1:def 7;
then k + k2 in dom D2 by FINSEQ_1:def 3;
then A522: (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k = (lower_bound (rng (f | (divset (D2,(k + k2)))))) * (vol (divset (D2,(k + k2)))) by A518, A520, INTEGRA1:def 7;
A523: k in Seg (len MD2) by A517, INTEGRA1:def 7;
A524: ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) )

proof

k + k2 >= 1 + 1 by A260, A515, A520, XREAL_1:7;
then A525: k + k2 > 1 by NAT_1:13;
A526: k in dom MD2 by A523, FINSEQ_1:def 3;
A527: k + k2 in dom D2 by A521, FINSEQ_1:def 3;

per cases ;

suppose A528: k = 1 ; :: thesis:

then upper_bound (divset (MD2,k)) = MD2 . k by A526, INTEGRA1:def 4;
then A529: upper_bound (divset (MD2,k)) = D2 . ((k + ((indx (D2,D1,n1)) + 1)) - 1) by A272, A263, A358, A388, A390, A445, A515, A516, FINSEQ_6:122;
A530: lower_bound (divset (D2,(k + k2))) = D2 . ((k + k2) - 1) by A525, A527, INTEGRA1:def 4;
lower_bound (divset (MD2,k)) = D1 . n1 by A354, A526, A528, INTEGRA1:def 4;
hence ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) ) by A13, A241, A520, A525, A527, A528, A529, A530, INTEGRA1:def 4, INTEGRA1:def 19; :: thesis:

end;

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

then upper_bound (divset (MD2,k)) = MD2 . k by A526, INTEGRA1:def 4;
then A532: upper_bound (divset (MD2,k)) = D2 . ((k + ((indx (D2,D1,n1)) + 1)) - 1) by A272, A263, A358, A388, A390, A445, A515, A516, FINSEQ_6:122;
A533: k - 1 <= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A445, A516, XREAL_1:146, XXREAL_0:2;
A534: lower_bound (divset (MD2,k)) = MD2 . (k - 1) by A526, A531, INTEGRA1:def 4;
A535: k - 1 in dom MD2 by A526, A531, INTEGRA1:7;
then 1 <= k - 1 by FINSEQ_3:25;
then lower_bound (divset (MD2,k)) = D2 . (((k - 1) + ((indx (D2,D1,n1)) + 1)) - 1) by A272, A263, A358, A388, A390, A535, A533, A534, FINSEQ_6:122;
hence ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) ) by A520, A525, A527, A532, INTEGRA1:def 4; :: thesis:

end;

divset (MD2,k) = [.(lower_bound (divset (MD2,k))),(upper_bound (divset (MD2,k))).] by INTEGRA1:4;
then A536: divset (MD2,k) = divset (D2,(k + k2)) by A524, INTEGRA1:4;
k in dom MD2 by A523, FINSEQ_1:def 3;
then divset (D2,(k + k2)) c= B by A536, INTEGRA1:8;
then A537: rng (f | (divset (D2,(k + k2)))) = rng (g | (divset (D2,(k + k2)))) by FUNCT_1:51;
k in dom MD2 by A523, FINSEQ_1:def 3;
hence (lower_volume (g,MD2)) . k = (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k by A522, A536, A537, INTEGRA1:def 7; :: thesis:

end;

lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;
then A538: D . (i + 1) in divset (MD1,(len MD1)) by A374, A512, INTEGRA2:1;
j - 1 in dom D1 by A236, A245, A280, INTEGRA1:7;
then D1 . n1 < D1 . (j - 1) by A241, A441, SEQM_3:def 1;
then D . (i + 1) > lower_bound B by A354, A511, XXREAL_0:2;
then (Sum (lower_volume (g,MD2))) - (Sum (lower_volume (g,MD1))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A356, A431, A488, A538, A387, Th13;
then A539: (Sum (lower_volume (g,MD2))) - (Sum (lower_volume (g,MD1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A440, XXREAL_0:2;
(indx (D2,D1,n1)) + 1 <= len H₁(D2) by A386, INTEGRA1:def 7;
then len (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) = ((indx (D2,D1,j)) -' ((indx (D2,D1,n1)) + 1)) + 1 by A262, A388, A442, A513, FINSEQ_6:118;
then len (lower_volume (g,MD2)) = len (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) by A272, A385, A445, XREAL_1:233, XXREAL_0:2;
then A540: Sum (lower_volume (g,MD2)) = Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) by A514, FINSEQ_1:14;
n1 + 1 <= len H₁(D1) by A267, INTEGRA1:def 7;
then len (mid (H₁(D1),(n1 + 1),j)) = (j -' (n1 + 1)) + 1 by A257, A265, A244, A407, FINSEQ_6:118
.= (j - (n1 + 1)) + 1 by A257, XREAL_1:233 ;
then Sum (lower_volume (g,MD1)) = Sum (mid (H₁(D1),(n1 + 1),j)) by A371, A408, FINSEQ_1:14;
hence (Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A539, A510, A540, XXREAL_0:2; :: thesis:

end;

hence (Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) ; :: thesis:

end;

then A541: (H₂(D2, indx (D2,D1,n1)) - H₂(D1,n1)) + ((Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j)))) <= ((i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)) + (((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)) by A243, XREAL_1:7;
n1 < n1 + 1 by NAT_1:13;
then D1 . n1 < D1 . (n1 + 1) by A241, A268, SEQM_3:def 1;
then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A259, A274, A269, A271, SEQ_4:137;
then A542: indx (D2,D1,n1) < indx (D2,D1,j) by A272, XXREAL_0:2;
indx (D2,D1,n1) in Seg (len D2) by A259, FINSEQ_1:def 3;
then indx (D2,D1,n1) in Seg (len H₁(D2)) by INTEGRA1:def 7;
then indx (D2,D1,n1) in dom H₁(D2) by FINSEQ_1:def 3;
then H₂(D2, indx (D2,D1,n1)) = Sum (H₁(D2) | (indx (D2,D1,n1))) by INTEGRA1:def 20
.= Sum (mid (H₁(D2),1,(indx (D2,D1,n1)))) by A260, FINSEQ_6:116 ;
then H₂(D2, indx (D2,D1,n1)) + (Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) = Sum ((mid (H₁(D2),1,(indx (D2,D1,n1)))) ^ (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) by RVSUM_1:75
.= Sum (mid (H₁(D2),1,(indx (D2,D1,j)))) by A260, A542, A264, INTEGRA2:4
.= Sum (H₁(D2) | (indx (D2,D1,j))) by A262, FINSEQ_6:116 ;
then H₂(D2, indx (D2,D1,j)) = H₂(D2, indx (D2,D1,n1)) + (Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) by A279, INTEGRA1:def 20;
then (H₂(D2, indx (D2,D1,n1)) - H₂(D1,n1)) + ((Sum (mid (H₁(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H₁(D1),(n1 + 1),j)))) = H₂(D2, indx (D2,D1,j)) - H₂(D1,j) by A278;
hence ex j being Element of NAT st
( j in dom D1 & D . (i + 1) in divset (D1,j) & H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= ((i + 1) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A236, A237, A541; :: thesis:

end;

hence S₁[i + 1] ; :: thesis:

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A40, A231);
then S₁[i] ;
hence ex j being Element of NAT st
( j in dom D1 & D . i in divset (D1,j) & H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A17; :: thesis:

end;

A543: len D1 in dom D1 by FINSEQ_5:6;
then D1 . (len D1) = D2 . (indx (D2,D1,(len D1))) by A13, INTEGRA1:def 19;
then upper_bound A = D2 . (indx (D2,D1,(len D1))) by INTEGRA1:def 2;
then A544: D2 . (len D2) = D2 . (indx (D2,D1,(len D1))) by INTEGRA1:def 2;
len D in dom D by FINSEQ_5:6;
then consider j being Element of NAT such that
A545: j in dom D1 and
A546: D . (len D) in divset (D1,j) and
A547: H₂(D2, indx (D2,D1,j)) - H₂(D1,j) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A16;
A548: j = len D1

proof

assume A549: j <> len D1 ; :: thesis:
j <= len D1 by A545, FINSEQ_3:25;
then j < len D1 by A549, XXREAL_0:1;
then D1 . j < D1 . (len D1) by A545, A543, SEQM_3:def 1;
then A550: D1 . j < upper_bound A by INTEGRA1:def 2;
A551: upper_bound (divset (D1,j)) < upper_bound A

proof

per cases ;

suppose j = 1 ; :: thesis:

hence upper_bound (divset (D1,j)) < upper_bound A by A545, A550, INTEGRA1:def 4; :: thesis:

end;

suppose j <> 1 ; :: thesis:

hence upper_bound (divset (D1,j)) < upper_bound A by A545, A550, INTEGRA1:def 4; :: thesis:

end;

D . (len D) <= upper_bound (divset (D1,j)) by A546, INTEGRA2:1;
hence contradiction by A551, INTEGRA1:def 2; :: thesis:

end;

indx (D2,D1,(len D1)) in dom D2 by A13, A543, INTEGRA1:def 19;
then indx (D2,D1,(len D1)) = len D2 by A15, A544, SEQ_4:138;
then H₂(D2, len D2) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A547, A548, INTEGRA1:43;
hence (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by INTEGRA1:43; :: thesis:

end;

hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A12, A13, A14; :: thesis:

end;

hence for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds
ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) ; :: thesis: