let A be closed-interval Subset of REAL ; :: thesis:
let f be Function of A,REAL ; :: thesis:
let T be DivSequence of A; :: thesis:
assume A1: f | A is bounded ; :: thesis:
A2: 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 <= (upper_sum f,D) - (upper_sum f,D2) & 0 <= (upper_sum f,D1) - (upper_sum f,D2) )

proof

let D, D1 be Division of A; :: thesis:
consider D2 being Division of A such that
A3: D <= D2 and
A4: D1 <= D2 and
A5: rng D2 = (rng D1) \/ (rng D) by Th3;
A6: (upper_sum f,D1) - (upper_sum f,D2) >= 0 by A1, A4, INTEGRA1:47, XREAL_1:50;
(upper_sum f,D) - (upper_sum f,D2) >= 0 by A1, A3, INTEGRA1:47, XREAL_1:50;
hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum f,D) - (upper_sum f,D2) & 0 <= (upper_sum f,D1) - (upper_sum f,D2) ) by A3, A4, A5, A6; :: thesis:

end;

A7: 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) & (upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

let D, D1 be Division of A; :: thesis:
assume A8: 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) & (upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

consider D2 being Division of A such that
A9: D <= D2 and
A10: D1 <= D2 and
A11: rng D2 = (rng D1) \/ (rng D) and
0 <= (upper_sum f,D) - (upper_sum f,D2) and
0 <= (upper_sum f,D1) - (upper_sum f,D2) by A2;
(upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

deffunc H₁( Division of A) -> FinSequence of REAL = upper_volume f,$1;
deffunc H₂( Division of A, Nat) -> Element of REAL = (PartSums (upper_volume f,$1)) . $2;
A12: len D2 in dom D2 by FINSEQ_5:6;
A13: 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₂(D1,j) - H₂(D2, indx D2,D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

defpred S₁[ non empty 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₂(D1,j) - H₂(D2, indx D2,D1,j) <= ($1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) );
let i be Element of NAT ; :: thesis:
assume A14: i in dom D ; :: thesis:
then A15: i in Seg (len D) by FINSEQ_1:def 3;
A16: 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 A17: i in dom D ; :: thesis:
assume that
A18: j in dom D1 and
A19: D . i in divset D1,j ; :: thesis:
assume j < 2 ; :: thesis:
then j < 1 + 1 ;
then A20: j <= 1 by NAT_1:13;
j in Seg (len D1) by A18, FINSEQ_1:def 3;
then j >= 1 by FINSEQ_1:3;
then j = 1 by A20, XXREAL_0:1;
then A21: lower_bound (divset D1,j) = lower_bound A by A18, INTEGRA1:def 5;
A22: D . i <= upper_bound (divset D1,j) by A19, INTEGRA2:1;
delta D1 >= min (rng (upper_volume (chi A,A),D))

proof

per cases ;

suppose A23: i = 1 ; :: thesis:

len D in Seg (len D) by FINSEQ_1:5;
then 1 <= len D by FINSEQ_1:3;
then A24: 1 in dom D by FINSEQ_3:27;
then A25: lower_bound (divset D,1) = lower_bound A by INTEGRA1:def 5;
1 in Seg (len D) by A24, FINSEQ_1:def 3;
then 1 in Seg (len (upper_volume (chi A,A),D)) by INTEGRA1:def 7;
then A26: 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 A24, INTEGRA1:22;
then vol (divset D,1) in rng (upper_volume (chi A,A),D) by A26, FUNCT_1:def 5;
then A27: vol (divset D,1) >= min (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 7;
A28: upper_bound (divset D,1) = D . 1 by A24, INTEGRA1:def 5;
(upper_bound (divset D1,j)) - (lower_bound A) >= (D . 1) - (lower_bound A) by A22, A23, XREAL_1:11;
then vol (divset D1,j) >= (upper_bound (divset D,1)) - (lower_bound (divset D,1)) by A21, A25, A28, INTEGRA1:def 6;
then A29: vol (divset D1,j) >= vol (divset D,1) by INTEGRA1:def 6;
vol (divset D1,j) <= delta D1 by A18, Lm5;
then delta D1 >= vol (divset D,1) by A29, XXREAL_0:2;
hence delta D1 >= min (rng (upper_volume (chi A,A),D)) by A27, XXREAL_0:2; :: thesis:

end;

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

then D . (i - 1) in A by A17, INTEGRA1:9;
then A31: lower_bound A <= D . (i - 1) by INTEGRA2:1;
lower_bound (divset D,i) = D . (i - 1) by A17, A30, INTEGRA1:def 5;
then A32: (upper_bound (divset D,i)) - (lower_bound A) >= (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A31, XREAL_1:12;
upper_bound (divset D,i) = D . i by A17, A30, INTEGRA1:def 5;
then (upper_bound (divset D1,j)) - (lower_bound (divset D1,j)) >= (upper_bound (divset D,i)) - (lower_bound A) by A22, A21, XREAL_1:11;
then (upper_bound (divset D1,j)) - (lower_bound (divset D1,j)) >= (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A32, XXREAL_0:2;
then vol (divset D1,j) >= (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by INTEGRA1:def 6;
then A33: vol (divset D1,j) >= vol (divset D,i) by INTEGRA1:def 6;
i in Seg (len D) by A17, FINSEQ_1:def 3;
then i in Seg (len (upper_volume (chi A,A),D)) by INTEGRA1:def 7;
then A34: 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 A17, INTEGRA1:22;
then vol (divset D,i) in rng (upper_volume (chi A,A),D) by A34, FUNCT_1:def 5;
then A35: vol (divset D,i) >= min (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 7;
vol (divset D1,j) <= delta D1 by A18, Lm5;
then delta D1 >= vol (divset D,i) by A33, XXREAL_0:2;
hence delta D1 >= min (rng (upper_volume (chi A,A),D)) by A35, XXREAL_0:2; :: thesis:

end;

hence contradiction by A8; :: thesis:

end;

A36: S₁[1]

proof

len D in Seg (len D) by FINSEQ_1:5;
then 1 <= len D by FINSEQ_1:3;
then A37: 1 in dom D by FINSEQ_3:27;
then consider j being Element of NAT such that
A38: j in dom D1 and
A39: D . 1 in divset D1,j by Th2, INTEGRA1:8;
H₂(D1,j) - H₂(D2, indx D2,D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

A40: j <> 1 by A16, A37, A38, A39;
then reconsider j1 = j - 1 as Element of NAT by A38, INTEGRA1:9;
A41: j1 in dom D1 by A38, A40, INTEGRA1:9;
then j1 in Seg (len D1) by FINSEQ_1:def 3;
then j1 in Seg (len (upper_volume f,D1)) by INTEGRA1:def 7;
then A42: j1 in dom (upper_volume f,D1) by FINSEQ_1:def 3;
A43: j - 1 in dom D1 by A38, A40, INTEGRA1:9;
then A44: indx D2,D1,j1 in dom D2 by A10, INTEGRA1:def 21;
then A45: indx D2,D1,j1 in Seg (len D2) by FINSEQ_1:def 3;
then A46: 1 <= indx D2,D1,j1 by FINSEQ_1:3;
then mid D2,1,(indx D2,D1,j1) is increasing by A44, INTEGRA1:37;
then A47: D2 | (indx D2,D1,j1) is increasing by A46, JORDAN3:25;
j < j + 1 by NAT_1:13;
then j1 < j by XREAL_1:21;
then A48: indx D2,D1,j1 < indx D2,D1,j by A10, A38, A41, Th7;
then A49: (indx D2,D1,j1) + 1 <= indx D2,D1,j by NAT_1:13;
A50: (Sum (mid (upper_volume f,D1),j,j)) - (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof

A51: (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 A52: (indx D2,D1,j1) + (1 + 1) < indx D2,D1,j by XREAL_1:22;
A53: ID1 < ID2 by NAT_1:13;
then indx D2,D1,j1 <= ID2 by NAT_1:13;
then A54: 1 <= ID2 by A46, XXREAL_0:2;
A55: indx D2,D1,j in dom D2 by A10, A38, INTEGRA1:def 21;
then A56: indx D2,D1,j <= len D2 by FINSEQ_3:27;
then ID2 <= len D2 by A52, XXREAL_0:2;
then A57: ID2 in dom D2 by A54, FINSEQ_3:27;
then A58: D2 . ID2 < D2 . (indx D2,D1,j) by A52, A55, SEQM_3:def 1;
A59: 1 <= ID1 by A46, NAT_1:13;
A60: D1 . j = D2 . (indx D2,D1,j) by A10, A38, INTEGRA1:def 21;
ID1 <= indx D2,D1,j by A52, A53, XXREAL_0:2;
then ID1 <= len D2 by A56, XXREAL_0:2;
then A61: ID1 in dom D2 by A59, FINSEQ_3:27;
then A62: D2 . ID1 < D2 . ID2 by A53, A57, SEQM_3:def 1;
indx D2,D1,j1 < ID1 by NAT_1:13;
then A63: D2 . (indx D2,D1,j1) < D2 . ID1 by A44, A61, SEQM_3:def 1;
A64: D1 . j1 = D2 . (indx D2,D1,j1) by A10, A41, INTEGRA1:def 21;
A65: ( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

proof

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

per cases by A66;

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

then consider n being Element of NAT such that
A67: n in dom D1 and
A68: D1 . n = D2 . ID1 by PARTFUN1:26;
j1 < n by A41, A63, A64, A67, A68, GOBOARD2:18;
then A69: j < n + 1 by XREAL_1:21;
D2 . ID1 < D2 . (indx D2,D1,j) by A62, A58, XXREAL_0:2;
then n < j by A38, A60, A67, A68, GOBOARD2:18;
hence contradiction by A69, NAT_1:13; :: thesis:

end;

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

then consider n being Element of NAT such that
A70: n in dom D1 and
A71: D1 . n = D2 . ID2 by PARTFUN1:26;
D2 . (indx D2,D1,j1) < D2 . ID2 by A63, A62, XXREAL_0:2;
then j1 < n by A41, A64, A70, A71, GOBOARD2:18;
then A72: j < n + 1 by XREAL_1:21;
n < j by A38, A58, A60, A70, A71, GOBOARD2:18;
hence contradiction by A72, NAT_1:13; :: thesis:

end;

upper_bound (divset D1,j) = D1 . j by A38, A40, INTEGRA1:def 5;
then A73: upper_bound (divset D1,j) = D2 . (indx D2,D1,j) by A10, A38, INTEGRA1:def 21;
lower_bound (divset D1,j) = D1 . j1 by A38, A40, INTEGRA1:def 5;
then A74: lower_bound (divset D1,j) = D2 . (indx D2,D1,j1) by A10, A41, INTEGRA1:def 21;
D2 . ID2 in rng D2 by A57, FUNCT_1:def 5;
then A75: D2 . ID2 in rng D by A11, A65, XBOOLE_0:def 3;
D2 . ID1 in rng D2 by A61, FUNCT_1:def 5;
then A76: D2 . ID1 in rng D by A11, A65, XBOOLE_0:def 3;
D2 . (indx D2,D1,j1) <= D2 . ID2 by A63, A62, XXREAL_0:2;
then D2 . ID2 in divset D1,j by A58, A74, A73, INTEGRA2:1;
then A77: D2 . ID2 in (rng D) /\ (divset D1,j) by A75, XBOOLE_0:def 4;
D2 . ID1 <= D2 . (indx D2,D1,j) by A62, A58, XXREAL_0:2;
then D2 . ID1 in divset D1,j by A63, A74, A73, INTEGRA2:1;
then D2 . ID1 in (rng D) /\ (divset D1,j) by A76, XBOOLE_0:def 4;
hence contradiction by A8, A38, A53, A61, A57, A77, Th4, GOBOARD2:19; :: thesis:

end;

A78: 1 <= (indx D2,D1,j1) + 1 by A46, NAT_1:13;
j <= len D1 by A38, FINSEQ_3:27;
then A79: j <= len (upper_volume f,D1) by INTEGRA1:def 7;
A80: 1 <= j by A38, FINSEQ_3:27;
then A81: (mid (upper_volume f,D1),j,j) . 1 = (upper_volume f,D1) . j by A79, JORDAN3:27;
(j -' j) + 1 = 1 by Lm1;
then len (mid (upper_volume f,D1),j,j) = 1 by A80, A79, JORDAN3:27;
then mid (upper_volume f,D1),j,j = <*((upper_volume f,D1) . j)*> by A81, FINSEQ_1:57;
then A82: Sum (mid (upper_volume f,D1),j,j) = (upper_volume f,D1) . j by FINSOP_1:12;
indx D2,D1,j in dom D2 by A10, A38, INTEGRA1:def 21;
then A83: indx D2,D1,j in Seg (len D2) by FINSEQ_1:def 3;
then A84: 1 <= indx D2,D1,j by FINSEQ_1:3;
indx D2,D1,j in Seg (len (upper_volume f,D2)) by A83, INTEGRA1:def 7;
then A85: indx D2,D1,j <= len (upper_volume f,D2) by FINSEQ_1:3;
then A86: (indx D2,D1,j1) + 1 <= len (upper_volume f,D2) by A49, XXREAL_0:2;
then (indx D2,D1,j1) + 1 in Seg (len (upper_volume f,D2)) by A78, FINSEQ_1:3;
then A87: (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7;
then A88: (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 A49, XREAL_1:235;
then ((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 <= 2 by A51;
then A89: len (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) <= 2 by A49, A84, A85, A78, A86, JORDAN3:27;
((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 >= 0 + 1 by XREAL_1:8;
then A90: 1 <= len (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) by A49, A84, A85, A78, A86, JORDAN3:27;

now

per cases by A90, A89, Lm2;

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

end;

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

A101: (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 1 = (upper_volume f,D2) . ((indx D2,D1,j1) + 1) by A84, A85, A78, A86, JORDAN3:27;
A102: 2 + ((indx D2,D1,j1) + 1) >= 0 + 1 by XREAL_1:9;
(mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 2 = H₁(D2) . ((2 + ((indx D2,D1,j1) + 1)) -' 1) by A49, A84, A85, A78, A86, A100, JORDAN3:27
.= H₁(D2) . ((2 + ((indx D2,D1,j1) + 1)) - 1) by A102, XREAL_1:235
.= H₁(D2) . ((indx D2,D1,j1) + (1 + 1)) ;
then mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j) = <*((upper_volume f,D2) . ((indx D2,D1,j1) + 1)),((upper_volume f,D2) . ((indx D2,D1,j1) + 2))*> by A100, A101, FINSEQ_1:61;
then A103: Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) = ((upper_volume f,D2) . ((indx D2,D1,j1) + 1)) + ((upper_volume f,D2) . ((indx D2,D1,j1) + 2)) by RVSUM_1:107;
A104: vol (divset D2,((indx D2,D1,j1) + 1)) >= 0 by INTEGRA1:11;
upper_bound (divset D1,j) = D1 . j by A38, A40, INTEGRA1:def 5;
then A105: upper_bound (divset D1,j) = D2 . (indx D2,D1,j) by A10, A38, INTEGRA1:def 21;
A106: vol (divset D2,((indx D2,D1,j1) + 2)) >= 0 by INTEGRA1:11;
((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A49, A84, A85, A78, A86, A100, JORDAN3:27;
then A107: 2 = ((indx D2,D1,j) - ((indx D2,D1,j1) + 1)) + 1 by A49, XREAL_1:235
.= (indx D2,D1,j) - (indx D2,D1,j1) ;
then A108: (indx D2,D1,j1) + 2 in dom D2 by A10, A38, INTEGRA1:def 21;
lower_bound (divset D1,j) = D1 . j1 by A38, A40, INTEGRA1:def 5;
then lower_bound (divset D1,j) = D2 . (indx D2,D1,j1) by A10, A41, INTEGRA1:def 21;
then A109: 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 A105, A107, INTEGRA1:def 6;
(indx D2,D1,j1) + 1 in Seg (len (upper_volume f,D2)) by A78, A86, FINSEQ_1:3;
then (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7;
then A110: (indx D2,D1,j1) + 1 in dom D2 by FINSEQ_1:def 3;
A111: (indx D2,D1,j1) + 1 <> 1 by A46, NAT_1:13;
then A112: upper_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . ((indx D2,D1,j1) + 1) by A110, INTEGRA1:def 5;
((indx D2,D1,j1) + 1) - 1 = (indx D2,D1,j1) + 0 ;
then A113: lower_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . (indx D2,D1,j1) by A110, A111, INTEGRA1:def 5;
A114: ((indx D2,D1,j1) + 1) + 1 > 1 by A78, NAT_1:13;
((indx D2,D1,j1) + 2) - 1 = (indx D2,D1,j1) + 1 ;
then A115: lower_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 1) by A108, A114, INTEGRA1:def 5;
upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2) by A108, A114, INTEGRA1:def 5;
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 A115, A109, INTEGRA1:def 6
.= (vol (divset D2,((indx D2,D1,j1) + 2))) + ((upper_bound (divset D2,((indx D2,D1,j1) + 1))) - (lower_bound (divset D2,((indx D2,D1,j1) + 1)))) by A113, A112 ;
then A116: vol (divset D1,j) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2))) by INTEGRA1:def 6;
then A117: (upper_volume f,D1) . j = (upper_bound (rng (f | (divset D1,j)))) * ((vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))) by A38, INTEGRA1:def 7;
A118: (Sum (mid H₁(D1),j,j)) - (Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,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 SR = upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))));
set VR = vol (divset D2,((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 A38, INTEGRA1:10;
then A119: upper_bound (rng (f | (divset D1,j))) <= upper_bound (rng f) by A1, Lm4;
(indx D2,D1,j1) + 1 in dom D2 by A87, FINSEQ_1:def 3;
then divset D2,((indx D2,D1,j1) + 1) c= A by INTEGRA1:10;
then upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1)))) >= lower_bound (rng f) by A1, Lm4;
then A120: (upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))) by A104, XREAL_1:66;
((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A49, A84, A85, A78, A86, A100, JORDAN3:27;
then A121: 2 = ((indx D2,D1,j) - ((indx D2,D1,j1) + 1)) + 1 by A49, XREAL_1:235
.= (indx D2,D1,j) - (indx D2,D1,j1) ;
A122: indx D2,D1,j in dom D2 by A10, A38, INTEGRA1:def 21;
then divset D2,((indx D2,D1,j1) + 2) c= A by A121, INTEGRA1:10;
then A123: upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 2)))) >= lower_bound (rng f) by A1, Lm4;
reconsider A = upper_bound (rng (f | (divset D1,j))) as real number ;
A124: ((upper_volume f,D1) . j) - (A * (vol (divset D2,((indx D2,D1,j1) + 1)))) = A * (vol (divset D2,((indx D2,D1,j1) + 2))) by A117;
(upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 2))) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2))) by A106, A119, XREAL_1:66;
then Sum (mid H₁(D1),j,j) <= ((upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) + ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) by A82, A124, XREAL_1:22;
then A125: (Sum (mid H₁(D1),j,j)) - ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) <= (upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by XREAL_1:22;
(upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 1))) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))) by A104, A119, XREAL_1:66;
then (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))) by A125, XXREAL_0:2;
then A126: 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)))) by XREAL_1:22;
Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) = ((upper_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 A103, A122, A121, INTEGRA1:def 7
.= ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 2))))) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) by A88, INTEGRA1:def 7 ;
then (Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) - ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2))) by A106, A123, XREAL_1:66;
then Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) >= ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) by XREAL_1:21;
then (Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) - ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) >= (upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by XREAL_1:21;
then (Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,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 A120, XXREAL_0:2;
then Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,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:21;
then (Sum (mid H₁(D1),j,j)) - (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))))) - (((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 A126, XREAL_1:15;
hence (Sum (mid H₁(D1),j,j)) - (Sum (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,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:50;
then ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset D1,j)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A38, Lm5, XREAL_1:66;
hence (Sum (mid (upper_volume f,D1),j,j)) - (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A116, A118, XXREAL_0:2; :: thesis:

end;

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

end;

j < j + 1 by NAT_1:13;
then A127: j1 < j by XREAL_1:21;
indx D2,D1,j in dom D2 by A10, A38, INTEGRA1:def 21;
then A128: indx D2,D1,j in Seg (len D2) by FINSEQ_1:def 3;
then A129: 1 <= indx D2,D1,j by FINSEQ_1:3;
A130: indx D2,D1,j1 <= len D2 by A45, FINSEQ_1:3;
then A131: len (D2 | (indx D2,D1,j1)) = indx D2,D1,j1 by FINSEQ_1:80;
A132: j1 in Seg (len D1) by A43, FINSEQ_1:def 3;
then A133: j1 <= len D1 by FINSEQ_1:3;
for x1 being set st x1 in rng (D1 | j1) holds
x1 in rng (D2 | (indx D2,D1,j1))

proof

let x1 be set ; :: thesis:
assume x1 in rng (D1 | j1) ; :: thesis:
then consider k being Element of NAT such that
A134: k in dom (D1 | j1) and
A135: x1 = (D1 | j1) . k by PARTFUN1:26;
k in Seg (len (D1 | j1)) by A134, FINSEQ_1:def 3;
then A136: k in Seg j1 by A133, FINSEQ_1:80;
then A137: k in dom D1 by A41, RFINSEQ:19;
k <= j1 by A136, FINSEQ_1:3;
then D1 . k <= D1 . j1 by A43, A137, GOBOARD2:18;
then D2 . (indx D2,D1,k) <= D1 . j1 by A10, A137, INTEGRA1:def 21;
then A138: D2 . (indx D2,D1,k) <= D2 . (indx D2,D1,j1) by A10, A43, INTEGRA1:def 21;
A139: (D1 | j1) . k = D1 . k by A41, A136, RFINSEQ:19;
D1 . k in rng D1 by A137, FUNCT_1:def 5;
then x1 in rng D2 by A11, A135, A139, XBOOLE_0:def 3;
then consider n being Element of NAT such that
A140: n in dom D2 and
A141: x1 = D2 . n by PARTFUN1:26;
D2 . (indx D2,D1,k) = D2 . n by A10, A135, A139, A137, A141, INTEGRA1:def 21;
then A142: n <= indx D2,D1,j1 by A44, A140, A138, SEQM_3:def 1;
1 <= n by A140, FINSEQ_3:27;
then A143: n in Seg (indx D2,D1,j1) by A142, FINSEQ_1:3;
then n in Seg (len (D2 | (indx D2,D1,j1))) by A130, FINSEQ_1:80;
then A144: n in dom (D2 | (indx D2,D1,j1)) by FINSEQ_1:def 3;
D2 . n = (D2 | (indx D2,D1,j1)) . n by A44, A143, RFINSEQ:19;
hence x1 in rng (D2 | (indx D2,D1,j1)) by A141, A144, FUNCT_1:def 5; :: thesis:

end;

then A145: rng (D1 | j1) c= rng (D2 | (indx D2,D1,j1)) by TARSKI:def 3;
A146: 1 <= j1 by A132, FINSEQ_1:3;
lower_bound (divset D1,j) <= D . 1 by A39, INTEGRA2:1;
then A147: D1 . j1 <= D . 1 by A38, A40, INTEGRA1:def 5;
for x1 being set st x1 in rng (D2 | (indx D2,D1,j1)) holds
x1 in rng (D1 | j1)

proof

let x1 be set ; :: thesis:
assume x1 in rng (D2 | (indx D2,D1,j1)) ; :: thesis:
then consider k being Element of NAT such that
A148: k in dom (D2 | (indx D2,D1,j1)) and
A149: x1 = (D2 | (indx D2,D1,j1)) . k by PARTFUN1:26;
k in Seg (len (D2 | (indx D2,D1,j1))) by A148, FINSEQ_1:def 3;
then A150: k in Seg (indx D2,D1,j1) by A130, FINSEQ_1:80;
then A151: k in dom D2 by A44, RFINSEQ:19;
A152: len (D1 | j1) = j1 by A133, FINSEQ_1:80;
k <= indx D2,D1,j1 by A150, FINSEQ_1:3;
then D2 . k <= D2 . (indx D2,D1,j1) by A44, A151, GOBOARD2:18;
then A153: D2 . k <= D1 . j1 by A10, A43, INTEGRA1:def 21;
A154: ( 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
A155: m in dom D1 and
A156: D2 . k = D1 . m by PARTFUN1:26;
m in Seg (len D1) by A155, FINSEQ_1:def 3;
then A157: 1 <= m by FINSEQ_1:3;
A158: m <= j1 by A41, A153, A155, A156, SEQM_3:def 1;
then m in Seg (len (D1 | j1)) by A152, A157, FINSEQ_1:3;
then A159: m in dom (D1 | j1) by FINSEQ_1:def 3;
m in Seg j1 by A157, A158, FINSEQ_1:3;
then D2 . k = (D1 | j1) . m by A41, A156, RFINSEQ:19;
hence D2 . k in rng (D1 | j1) by A159, FUNCT_1:def 5; :: thesis:

end;

A160: ( 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
A161: n in dom D and
A162: D2 . k = D . n by PARTFUN1:26;
1 <= n by A161, FINSEQ_3:27;
then D . 1 <= D2 . k by A37, A161, A162, GOBOARD2:18;
then D1 . j1 <= D2 . k by A147, XXREAL_0:2;
hence D2 . k = D1 . j1 by A153, XXREAL_0:1; :: thesis:

end;

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

proof

j1 in Seg (len (D1 | j1)) by A146, A152, FINSEQ_1:3;
then j1 in dom (D1 | j1) by FINSEQ_1:def 3;
then A164: (D1 | j1) . j1 in rng (D1 | j1) by FUNCT_1:def 5;
assume A165: D2 . k in rng D ; :: thesis:
j1 in Seg j1 by A146, FINSEQ_1:3;
hence D2 . k in rng (D1 | j1) by A41, A160, A165, A164, RFINSEQ:19; :: thesis:

end;

D2 . k in rng D2 by A151, FUNCT_1:def 5;
hence x1 in rng (D1 | j1) by A11, A44, A149, A150, A163, A154, RFINSEQ:19, XBOOLE_0:def 3; :: thesis:

end;

then rng (D2 | (indx D2,D1,j1)) c= rng (D1 | j1) by TARSKI:def 3;
then A166: rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1) by A145, XBOOLE_0:def 10;
mid D1,1,j1 is increasing by A38, A40, A146, INTEGRA1:9, INTEGRA1:37;
then A167: D1 | j1 is increasing by A146, JORDAN3:25;
then A168: D2 | (indx D2,D1,j1) = D1 | j1 by A47, A166, Th5;
A169: 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
A170: 1 <= k and
A171: k <= j1 ; :: thesis:
assume A172: k <> indx D2,D1,k ; :: thesis:

now

per cases by A172, XXREAL_0:1;

suppose A173: k > indx D2,D1,k ; :: thesis:

k <= len D1 by A133, A171, XXREAL_0:2;
then A174: k in dom D1 by A170, FINSEQ_3:27;
then indx D2,D1,k in dom D2 by A10, INTEGRA1:def 21;
then indx D2,D1,k in Seg (len D2) by FINSEQ_1:def 3;
then A175: 1 <= indx D2,D1,k by FINSEQ_1:3;
A176: indx D2,D1,k < j1 by A171, A173, XXREAL_0:2;
then A177: indx D2,D1,k in Seg j1 by A175, FINSEQ_1:3;
indx D2,D1,k <= indx D2,D1,j1 by A10, A41, A171, A174, Th6;
then indx D2,D1,k in Seg (indx D2,D1,j1) by A175, FINSEQ_1:3;
then A178: (D2 | (indx D2,D1,j1)) . (indx D2,D1,k) = D2 . (indx D2,D1,k) by A44, RFINSEQ:19;
indx D2,D1,k <= len D1 by A133, A176, XXREAL_0:2;
then indx D2,D1,k in dom D1 by A175, FINSEQ_3:27;
then A179: D1 . k > D1 . (indx D2,D1,k) by A173, A174, SEQM_3:def 1;
D1 . k = D2 . (indx D2,D1,k) by A10, A174, INTEGRA1:def 21;
hence contradiction by A41, A168, A178, A179, A177, RFINSEQ:19; :: thesis:

end;

suppose A180: k < indx D2,D1,k ; :: thesis:

k <= len D1 by A133, A171, XXREAL_0:2;
then A181: k in dom D1 by A170, FINSEQ_3:27;
then indx D2,D1,k <= indx D2,D1,j1 by A10, A41, A171, Th6;
then A182: k <= indx D2,D1,j1 by A180, XXREAL_0:2;
then k <= len D2 by A130, XXREAL_0:2;
then A183: k in dom D2 by A170, FINSEQ_3:27;
k in Seg j1 by A170, A171, FINSEQ_1:3;
then A184: D1 . k = (D1 | j1) . k by A43, RFINSEQ:19;
indx D2,D1,k in dom D2 by A10, A181, INTEGRA1:def 21;
then A185: D2 . k < D2 . (indx D2,D1,k) by A180, A183, SEQM_3:def 1;
A186: k in Seg (indx D2,D1,j1) by A170, A182, FINSEQ_1:3;
D1 . k = D2 . (indx D2,D1,k) by A10, A181, INTEGRA1:def 21;
hence contradiction by A44, A168, A184, A185, A186, RFINSEQ:19; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

proof

indx D2,D1,j1 in Seg (len D2) by A44, FINSEQ_1:def 3;
then indx D2,D1,j1 in Seg (len (upper_volume f,D2)) by INTEGRA1:def 7;
then A188: indx D2,D1,j1 in dom (upper_volume f,D2) by FINSEQ_1:def 3;
let k be Nat; :: thesis:
assume that
A189: 1 <= k and
A190: k <= len ((upper_volume f,D1) | j1) ; :: thesis:
A191: len (upper_volume f,D1) = len D1 by INTEGRA1:def 7;
then A192: k <= j1 by A133, A190, FINSEQ_1:80;
then A193: k in Seg j1 by A189, FINSEQ_1:3;
then indx D2,D1,k in Seg j1 by A169, A189, A192;
then A194: indx D2,D1,k in Seg (indx D2,D1,j1) by A146, A169;
then indx D2,D1,k <= indx D2,D1,j1 by FINSEQ_1:3;
then A195: indx D2,D1,k <= len D2 by A130, XXREAL_0:2;
k <= len D1 by A133, A192, XXREAL_0:2;
then A196: k in Seg (len D1) by A189, FINSEQ_1:3;
then A197: k in dom D1 by FINSEQ_1:def 3;
then A198: indx D2,D1,k in dom D2 by A10, INTEGRA1:def 21;
A199: D1 . k = D2 . (indx D2,D1,k) by A10, A197, INTEGRA1:def 21;
A200: ( 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 A201: k = 1 ; :: thesis:

then A202: upper_bound (divset D1,k) = D1 . k by A197, INTEGRA1:def 5;
A203: lower_bound (divset D1,k) = lower_bound A by A197, A201, INTEGRA1:def 5;
indx D2,D1,k = 1 by A146, A169, A201;
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 A198, A199, A203, A202, INTEGRA1:def 5; :: thesis:

end;

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

then reconsider k1 = k - 1 as Element of NAT by A197, INTEGRA1:9;
k <= k + 1 by NAT_1:11;
then k1 <= k by XREAL_1:22;
then A205: k1 <= j1 by A192, XXREAL_0:2;
A206: k - 1 in dom D1 by A197, A204, INTEGRA1:9;
then 1 <= k1 by FINSEQ_3:27;
then k1 = indx D2,D1,k1 by A169, A205;
then A207: D2 . ((indx D2,D1,k) - 1) = D2 . (indx D2,D1,k1) by A169, A189, A192, A193;
A208: indx D2,D1,k <> 1 by A169, A189, A192, A193, A204;
then A209: lower_bound (divset D2,(indx D2,D1,k)) = D2 . ((indx D2,D1,k) - 1) by A198, INTEGRA1:def 5;
A210: upper_bound (divset D2,(indx D2,D1,k)) = D2 . (indx D2,D1,k) by A198, A208, INTEGRA1:def 5;
A211: upper_bound (divset D1,k) = D1 . k by A197, A204, INTEGRA1:def 5;
lower_bound (divset D1,k) = D1 . (k - 1) by A197, A204, INTEGRA1:def 5;
hence ( lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) & upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) ) by A10, A197, A211, A206, A209, A210, A207, INTEGRA1:def 21; :: thesis:

end;

end;

indx D2,D1,j1 in dom D2 by A10, A43, INTEGRA1:def 21;
then indx D2,D1,j1 <= len D2 by FINSEQ_3:27;
then A216: indx D2,D1,j1 <= len (upper_volume f,D2) by INTEGRA1:def 7;
j1 <= len D1 by A43, FINSEQ_3:27;
then A217: j1 <= len (upper_volume f,D1) by INTEGRA1:def 7;
len (D2 | (indx D2,D1,j1)) = len (D1 | j1) by A47, A167, A166, Th5;
then indx D2,D1,j1 = j1 by A133, A131, FINSEQ_1:80;
then len ((upper_volume f,D1) | j1) = indx D2,D1,j1 by A217, FINSEQ_1:80;
then len ((upper_volume f,D1) | j1) = len ((upper_volume f,D2) | (indx D2,D1,j1)) by A216, FINSEQ_1:80;
then A218: (upper_volume f,D2) | (indx D2,D1,j1) = (upper_volume f,D1) | j1 by A187, FINSEQ_1:18;
A219: j in Seg (len D1) by A38, FINSEQ_1:def 3;
then A220: 1 <= j by FINSEQ_1:3;
indx D2,D1,j in Seg (len H₁(D2)) by A128, INTEGRA1:def 7;
then A221: indx D2,D1,j in dom H₁(D2) by FINSEQ_1:def 3;
indx D2,D1,j <= len D2 by A128, FINSEQ_1:3;
then A222: indx D2,D1,j <= len H₁(D2) by INTEGRA1:def 7;
j in Seg (len H₁(D1)) by A219, INTEGRA1:def 7;
then A223: j in dom H₁(D1) by FINSEQ_1:def 3;
j <= len D1 by A219, FINSEQ_1:3;
then A224: j <= len H₁(D1) by INTEGRA1:def 7;
j1 in Seg (len D1) by A41, FINSEQ_1:def 3;
then j1 in Seg (len H₁(D1)) by INTEGRA1:def 7;
then j1 in dom H₁(D1) by FINSEQ_1:def 3;
then H₂(D1,j1) = Sum (H₁(D1) | j1) by INTEGRA1:def 22;
then H₂(D1,j1) + (Sum (mid H₁(D1),j,j)) = Sum ((H₁(D1) | j1) ^ (mid H₁(D1),j,j)) by RVSUM_1:105
.= Sum ((mid H₁(D1),1,j1) ^ (mid H₁(D1),(j1 + 1),j)) by A146, JORDAN3:25
.= Sum (mid H₁(D1),1,j) by A146, A224, A127, INTEGRA2:4
.= Sum (H₁(D1) | j) by A220, JORDAN3:25 ;
then A225: H₂(D1,j1) + (Sum (mid (upper_volume f,D1),j,j)) = H₂(D1,j) by A223, INTEGRA1:def 22;
indx D2,D1,j1 in Seg (len D2) by A44, FINSEQ_1:def 3;
then indx D2,D1,j1 in Seg (len H₁(D2)) by INTEGRA1:def 7;
then indx D2,D1,j1 in dom H₁(D2) by FINSEQ_1:def 3;
then H₂(D2, indx D2,D1,j1) = Sum (H₁(D2) | (indx D2,D1,j1)) by INTEGRA1:def 22;
then H₂(D2, indx D2,D1,j1) + (Sum (mid (upper_volume 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:105
.= Sum ((mid H₁(D2),1,(indx D2,D1,j1)) ^ (mid H₁(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) by A46, JORDAN3:25
.= Sum (mid H₁(D2),1,(indx D2,D1,j)) by A46, A48, A222, INTEGRA2:4
.= Sum (H₁(D2) | (indx D2,D1,j)) by A129, JORDAN3:25 ;
then A226: H₂(D2, indx D2,D1,j1) + (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) = H₂(D2, indx D2,D1,j) by A221, INTEGRA1:def 22;
indx D2,D1,j1 in Seg (len D2) by A44, FINSEQ_1:def 3;
then indx D2,D1,j1 in Seg (len (upper_volume f,D2)) by INTEGRA1:def 7;
then indx D2,D1,j1 in dom (upper_volume f,D2) by FINSEQ_1:def 3;
then H₂(D2, indx D2,D1,j1) = Sum ((upper_volume f,D2) | (indx D2,D1,j1)) by INTEGRA1:def 22
.= H₂(D1,j1) by A218, A42, INTEGRA1:def 22 ;
hence H₂(D1,j) - H₂(D2, indx D2,D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A50, A226, A225; :: thesis:

end;

hence S₁[1] by A38, A39; :: thesis:

end;

reconsider i = i as non empty Element of NAT by A15, FINSEQ_1:3;
A227: for i being non empty Nat st S₁[i] holds
S₁[i + 1]

proof

let i be non empty Nat; :: thesis:
A228: i >= 1 by NAT_1:14;
assume A229: S₁[i] ; :: thesis:
S₁[i + 1]

proof

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

proof

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

now

per cases by A246, XXREAL_0:1;

suppose A247: n1 = j ; :: thesis:

D . i in rng D by A236, FUNCT_1:def 5;
then A248: D . i in (rng D) /\ (divset D1,j) by A242, A247, XBOOLE_0:def 4;
D . (i + 1) in rng D by A231, FUNCT_1:def 5;
then A249: D . (i + 1) in (rng D) /\ (divset D1,j) by A233, XBOOLE_0:def 4;
i + 1 > i by XREAL_1:31;
hence contradiction by A8, A231, A232, A236, A248, A249, Th4, GOBOARD2:19; :: thesis:

end;

suppose n1 > j ; :: thesis:

then A250: n1 >= j + 1 by NAT_1:13;
then A251: n1 - 1 >= j by XREAL_1:21;
1 <= j by A232, FINSEQ_3:27;
then 1 + 1 <= j + 1 by XREAL_1:8;
then A252: n1 <> 1 by A250, XXREAL_0:2;
then n1 - 1 in dom D1 by A241, INTEGRA1:9;
then A253: D1 . j <= D1 . (n1 - 1) by A232, A251, GOBOARD2:18;
A254: upper_bound (divset D1,j) = D1 . j

proof

per cases ;

suppose j = 1 ; :: thesis:

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

end;

suppose j <> 1 ; :: thesis:

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

end;

A255: lower_bound (divset D1,n1) <= D . i by A242, INTEGRA2:1;
lower_bound (divset D1,n1) = D1 . (n1 - 1) by A241, A252, INTEGRA1:def 5;
then A256: D . i >= D1 . j by A255, A253, XXREAL_0:2;
A257: i < i + 1 by XREAL_1:31;
D . (i + 1) <= upper_bound (divset D1,j) by A233, INTEGRA2:1;
then D . i >= D . (i + 1) by A254, A256, XXREAL_0:2;
hence contradiction by A231, A236, A257, SEQM_3:def 1; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A258: n1 + 1 <= j by NAT_1:13;
A259: 1 <= n1 by A241, FINSEQ_3:27;
A260: D2 . (indx D2,D1,n1) = D1 . n1 by A10, A241, INTEGRA1:def 21;
A261: 1 <= j by A232, FINSEQ_3:27;
A262: indx D2,D1,n1 in dom D2 by A10, A241, INTEGRA1:def 21;
then A263: 1 <= indx D2,D1,n1 by FINSEQ_3:27;
A264: j <= len D1 by A232, FINSEQ_3:27;
then A265: n1 + 1 <= len D1 by A258, XXREAL_0:2;
then A266: n1 + 1 in dom D1 by A244, FINSEQ_3:27;
then A267: D2 . (indx D2,D1,(n1 + 1)) = D1 . (n1 + 1) by A10, INTEGRA1:def 21;
A268: j <= len H₁(D1) by A264, INTEGRA1:def 7;
then j in Seg (len H₁(D1)) by A261, FINSEQ_1:3;
then A269: j in dom H₁(D1) by FINSEQ_1:def 3;
A270: indx D2,D1,(n1 + 1) in dom D2 by A10, A266, INTEGRA1:def 21;
then A271: 1 <= indx D2,D1,(n1 + 1) by FINSEQ_3:27;
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 22
.= Sum (mid H₁(D1),1,n1) by A259, JORDAN3:25 ;
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:105
.= Sum (mid H₁(D1),1,j) by A245, A259, A268, INTEGRA2:4
.= Sum (H₁(D1) | j) by A261, JORDAN3:25 ;
then A272: H₂(D1,j) = H₂(D1,n1) + (Sum (mid H₁(D1),(n1 + 1),j)) by A269, INTEGRA1:def 22;
indx D2,D1,j in Seg (len D2) by A237, FINSEQ_1:def 3;
then indx D2,D1,j in Seg (len H₁(D2)) by INTEGRA1:def 7;
then A273: indx D2,D1,j in dom H₁(D2) by FINSEQ_1:def 3;
A274: indx D2,D1,(n1 + 1) <= len D2 by A270, FINSEQ_3:27;
D1 . (n1 + 1) <= D1 . j by A232, A258, A266, GOBOARD2:18;
then A275: indx D2,D1,(n1 + 1) <= indx D2,D1,j by A270, A267, A237, A234, SEQM_3:def 1;
then 1 + (indx D2,D1,(n1 + 1)) <= (indx D2,D1,j) + 1 by XREAL_1:8;
then 1 <= ((indx D2,D1,j) + 1) - (indx D2,D1,(n1 + 1)) by XREAL_1:21;
then A276: (mid D2,(indx D2,D1,(n1 + 1)),(indx D2,D1,j)) . 1 = D2 . ((1 - 1) + (indx D2,D1,(n1 + 1))) by A275, A271, A239, JORDAN3:31
.= D1 . (n1 + 1) by A10, A266, INTEGRA1:def 21 ;
A277: n1 >= 1 by A241, FINSEQ_3:27;
A278: j - n1 >= 1 by A258, XREAL_1:21;
(Sum (mid H₁(D1),(n1 + 1),j)) - (Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof

per cases by A258, XXREAL_0:1;

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

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

proof

A281: upper_bound (divset D1,j) = D1 . j by A232, A245, A277, INTEGRA1:def 5;
A282: lower_bound (divset D1,j) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 5;
A283: 1 <= (indx D2,D1,n1) + 1 by A263, NAT_1:13;
assume (indx D2,D1,j) - (indx D2,D1,n1) > 2 ; :: thesis:
then A284: (indx D2,D1,n1) + 2 < indx D2,D1,j by XREAL_1:22;
then A285: (indx D2,D1,n1) + 2 <= len D2 by A239, XXREAL_0:2;
A286: (indx D2,D1,n1) + 1 < (indx D2,D1,n1) + 2 by XREAL_1:8;
then A287: indx D2,D1,n1 < (indx D2,D1,n1) + 2 by NAT_1:13;
then 1 <= (indx D2,D1,n1) + 2 by A263, XXREAL_0:2;
then A288: (indx D2,D1,n1) + 2 in dom D2 by A285, FINSEQ_3:27;
then A289: D2 . (indx D2,D1,j) >= D2 . ((indx D2,D1,n1) + 2) by A237, A284, GOBOARD2:18;
A290: 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
A291: k1 in dom D1 and
A292: D2 . ((indx D2,D1,n1) + 2) = D1 . k1 by PARTFUN1:26;
D2 . ((indx D2,D1,n1) + 2) < D2 . (indx D2,D1,j) by A237, A284, A288, SEQM_3:def 1;
then A293: k1 < j by A232, A234, A291, A292, GOBOARD2:18;
D2 . (indx D2,D1,n1) < D2 . ((indx D2,D1,n1) + 2) by A262, A287, A288, SEQM_3:def 1;
then n1 < k1 by A241, A260, A291, A292, GOBOARD2:18;
hence contradiction by A279, A293, NAT_1:13; :: thesis:

end;

D2 . ((indx D2,D1,n1) + 2) in rng D2 by A288, FUNCT_1:def 5;
then A294: D2 . ((indx D2,D1,n1) + 2) in rng D by A11, A290, XBOOLE_0:def 3;
A295: lower_bound (divset D1,j) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 5;
A296: upper_bound (divset D1,j) = D1 . j by A232, A245, A277, INTEGRA1:def 5;
D2 . ((indx D2,D1,n1) + 2) >= D2 . (indx D2,D1,n1) by A262, A287, A288, GOBOARD2:18;
then D2 . ((indx D2,D1,n1) + 2) in divset D1,j by A260, A234, A279, A295, A281, A289, INTEGRA2:1;
then A297: D2 . ((indx D2,D1,n1) + 2) in (rng D) /\ (divset D1,j) by A294, XBOOLE_0:def 4;
A298: (indx D2,D1,n1) + 1 < indx D2,D1,j by A284, A286, XXREAL_0:2;
then (indx D2,D1,n1) + 1 <= len D2 by A239, XXREAL_0:2;
then A299: (indx D2,D1,n1) + 1 in dom D2 by A283, FINSEQ_3:27;
then A300: D2 . (indx D2,D1,j) >= D2 . ((indx D2,D1,n1) + 1) by A237, A298, GOBOARD2:18;
A301: indx D2,D1,n1 < (indx D2,D1,n1) + 1 by NAT_1:13;
A302: 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
A303: k1 in dom D1 and
A304: D2 . ((indx D2,D1,n1) + 1) = D1 . k1 by PARTFUN1:26;
D2 . ((indx D2,D1,n1) + 1) < D2 . (indx D2,D1,j) by A237, A298, A299, SEQM_3:def 1;
then A305: k1 < j by A232, A234, A303, A304, GOBOARD2:18;
D2 . (indx D2,D1,n1) < D2 . ((indx D2,D1,n1) + 1) by A262, A301, A299, SEQM_3:def 1;
then n1 < k1 by A241, A260, A303, A304, GOBOARD2:18;
hence contradiction by A279, A305, NAT_1:13; :: thesis:

end;

D2 . ((indx D2,D1,n1) + 1) in rng D2 by A299, FUNCT_1:def 5;
then A306: D2 . ((indx D2,D1,n1) + 1) in rng D by A11, A302, XBOOLE_0:def 3;
D2 . ((indx D2,D1,n1) + 1) >= D2 . (indx D2,D1,n1) by A262, A301, A299, GOBOARD2:18;
then D2 . ((indx D2,D1,n1) + 1) in divset D1,j by A260, A234, A279, A282, A296, A300, INTEGRA2:1;
then D2 . ((indx D2,D1,n1) + 1) in (rng D) /\ (divset D1,j) by A306, XBOOLE_0:def 4;
then D2 . ((indx D2,D1,n1) + 1) = D2 . ((indx D2,D1,n1) + 2) by A8, A232, A297, Th4;
hence contradiction by A286, A299, A288, SEQM_3:def 1; :: thesis:

end;

A307: ( (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 A308: ((indx D2,D1,n1) + 1) + 1 <= indx D2,D1,j by NAT_1:13;
(indx D2,D1,n1) + 2 >= indx D2,D1,j by A280, XREAL_1:22;
hence (indx D2,D1,n1) + 2 = indx D2,D1,j by A308, XXREAL_0:1; :: thesis:

end;

A309: 1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
A310: indx D2,D1,j <= len H₁(D2) by A239, INTEGRA1:def 7;
D1 . n1 < D1 . j by A232, A241, A245, SEQM_3:def 1;
then A311: indx D2,D1,n1 < indx D2,D1,j by A262, A260, A237, A234, GOBOARD2:18;
then A312: (indx D2,D1,n1) + 1 <= indx D2,D1,j by NAT_1:13;
then (indx D2,D1,n1) + 1 <= len D2 by A239, XXREAL_0:2;
then (indx D2,D1,n1) + 1 <= len H₁(D2) by INTEGRA1:def 7;
then A313: len (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) = ((indx D2,D1,j) -' ((indx D2,D1,n1) + 1)) + 1 by A238, A312, A309, A310, JORDAN3:27
.= ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A312, XREAL_1:235
.= (indx D2,D1,j) - (indx D2,D1,n1) ;
(indx D2,D1,n1) + 1 <= indx D2,D1,j by A311, NAT_1:13;
then A314: ( (indx D2,D1,n1) + 1 = indx D2,D1,j or (indx D2,D1,n1) + 1 < indx D2,D1,j ) by XXREAL_0:1;
A315: Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1)))

proof

now

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

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

(indx D2,D1,n1) + 1 >= 1 + 1 by A263, XREAL_1:8;
then A317: (indx D2,D1,n1) + 1 <> 1 ;
then upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . ((indx D2,D1,n1) + 1) by A237, A316, INTEGRA1:def 5;
then A318: upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D1 . j by A10, A232, A316, INTEGRA1:def 21;
lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . (((indx D2,D1,n1) + 1) - 1) by A237, A316, A317, INTEGRA1:def 5;
then A319: lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D1 . n1 by A10, A241, INTEGRA1:def 21;
lower_bound (divset D1,(n1 + 1)) = D1 . ((n1 + 1) - 1) by A245, A277, A266, A279, INTEGRA1:def 5;
then A320: divset D2,((indx D2,D1,n1) + 1) = divset D1,(n1 + 1) by A245, A277, A266, A279, A319, A318, INTEGRA1:def 5;
A321: vol (divset D2,((indx D2,D1,n1) + 1)) >= 0 by INTEGRA1:11;
1 = ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A316;
then (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 1 = H₁(D2) . ((1 + ((indx D2,D1,n1) + 1)) - 1) by A309, A310, JORDAN3:31
.= H₁(D2) . ((indx D2,D1,n1) + 1) ;
then A322: mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j) = <*(H₁(D2) . ((indx D2,D1,n1) + 1))*> by A313, A316, FINSEQ_1:57;
H₁(D2) . ((indx D2,D1,n1) + 1) = (upper_bound (rng (f | (divset D2,((indx D2,D1,n1) + 1))))) * (vol (divset D2,((indx D2,D1,n1) + 1))) by A237, A316, INTEGRA1:def 7;
then H₁(D2) . ((indx D2,D1,n1) + 1) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A1, A237, A316, A320, A321, Th18, XREAL_1:66;
hence Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A322, FINSOP_1:12; :: thesis:

end;

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

(indx D2,D1,n1) + 2 >= 2 + 1 by A263, XREAL_1:8;
then A324: (indx D2,D1,n1) + 2 <> 1 ;
then A325: upper_bound (divset D2,((indx D2,D1,n1) + 2)) = D2 . (indx D2,D1,j) by A237, A323, INTEGRA1:def 5;
((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 A237, A323, A324, INTEGRA1:def 5;
then A326: vol (divset D2,((indx D2,D1,n1) + 2)) = (D1 . j) - (D2 . ((indx D2,D1,n1) + 1)) by A234, A325, INTEGRA1:def 6;
A327: upper_bound (divset D1,(n1 + 1)) = D1 . (n1 + 1) by A245, A277, A266, A279, INTEGRA1:def 5;
lower_bound (divset D1,(n1 + 1)) = D1 . ((n1 + 1) - 1) by A245, A277, A266, A279, INTEGRA1:def 5;
then A328: vol (divset D1,(n1 + 1)) = (D1 . (n1 + 1)) - (D1 . n1) by A327, INTEGRA1:def 6;
A329: vol (divset D2,((indx D2,D1,n1) + 2)) >= 0 by INTEGRA1:11;
A330: indx D2,D1,j <= len H₁(D2) by A239, INTEGRA1:def 7;
A331: vol (divset D2,((indx D2,D1,n1) + 1)) >= 0 by INTEGRA1:11;
A332: 1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
A333: (indx D2,D1,n1) + 1 <= (indx D2,D1,n1) + 2 by XREAL_1:8;
then (indx D2,D1,n1) + 1 <= len D2 by A239, A323, XXREAL_0:2;
then A334: (indx D2,D1,n1) + 1 in dom D2 by A332, FINSEQ_3:27;
then H₁(D2) . ((indx D2,D1,n1) + 1) = (upper_bound (rng (f | (divset D2,((indx D2,D1,n1) + 1))))) * (vol (divset D2,((indx D2,D1,n1) + 1))) by INTEGRA1:def 7;
then A335: H₁(D2) . ((indx D2,D1,n1) + 1) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1))) by A1, A334, A331, Th18, XREAL_1:66;
((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 = 1 + 1 by A323;
then A336: (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 2 = H₁(D2) . ((2 + ((indx D2,D1,n1) + 1)) - 1) by A332, A333, A330, JORDAN3:31
.= H₁(D2) . (((indx D2,D1,n1) + 0 ) + 2) ;
((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 >= 1 by A323;
then (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 1 = H₁(D2) . ((1 + ((indx D2,D1,n1) + 1)) - 1) by A323, A332, A333, A330, JORDAN3:31
.= 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 A313, A323, A336, FINSEQ_1:61;
then A337: 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:107;
A338: (indx D2,D1,n1) + 1 > 1 by A263, NAT_1:13;
then A339: upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . ((indx D2,D1,n1) + 1) by A334, INTEGRA1:def 5;
lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . (((indx D2,D1,n1) + 1) - 1) by A334, A338, INTEGRA1:def 5;
then A340: vol (divset D2,((indx D2,D1,n1) + 1)) = (D2 . ((indx D2,D1,n1) + 1)) - (D1 . n1) by A260, A339, INTEGRA1:def 6;
H₁(D2) . ((indx D2,D1,n1) + 2) = (upper_bound (rng (f | (divset D2,((indx D2,D1,n1) + 2))))) * (vol (divset D2,((indx D2,D1,n1) + 2))) by A237, A323, INTEGRA1:def 7;
then H₁(D2) . ((indx D2,D1,n1) + 2) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 2))) by A1, A237, A323, A329, Th18, XREAL_1:66;
then Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1)))) + ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 2)))) by A337, A335, XREAL_1:9;
hence Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A279, A340, A326, A328; :: thesis:

end;

hence Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) ; :: thesis:

end;

A341: delta D1 = max (rng (upper_volume (chi A,A),D1)) by INTEGRA1:def 19;
A342: n1 + 1 <= len H₁(D1) by A265, INTEGRA1:def 7;
(j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A279, XREAL_1:235;
then A343: len (mid H₁(D1),(n1 + 1),j) = 1 by A244, A279, A342, JORDAN3:27;
(n1 + 1) + 1 <= j + 1 by A258, XREAL_1:8;
then 1 <= (j + 1) - (n1 + 1) by XREAL_1:21;
then (mid H₁(D1),(n1 + 1),j) . 1 = H₁(D1) . ((1 + (n1 + 1)) - 1) by A244, A279, A342, JORDAN3:31
.= (upper_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))) by A266, INTEGRA1:def 7 ;
then mid H₁(D1),(n1 + 1),j = <*((upper_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))))*> by A343, FINSEQ_1:57;
then A344: Sum (mid H₁(D1),(n1 + 1),j) = (upper_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))) by FINSOP_1:12;
divset D1,(n1 + 1) c= A by A266, INTEGRA1:10;
then A345: upper_bound (rng (f | (divset D1,(n1 + 1)))) <= upper_bound (rng f) by A1, Lm4;
n1 + 1 in Seg (len D1) by A266, FINSEQ_1:def 3;
then n1 + 1 in Seg (len (upper_volume (chi A,A),D1)) by INTEGRA1:def 7;
then A346: 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 A266, INTEGRA1:22;
then vol (divset D1,(n1 + 1)) in rng (upper_volume (chi A,A),D1) by A346, FUNCT_1:def 5;
then A347: vol (divset D1,(n1 + 1)) <= delta D1 by A341, XXREAL_2:def 8;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:50;
then A348: ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset D1,(n1 + 1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A347, XREAL_1:66;
vol (divset D1,(n1 + 1)) >= 0 by INTEGRA1:11;
then Sum (mid H₁(D1),(n1 + 1),j) <= (upper_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A344, A345, XREAL_1:66;
then (Sum (mid H₁(D1),(n1 + 1),j)) - (Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) * (vol (divset D1,(n1 + 1)))) - ((lower_bound (rng f)) * (vol (divset D1,(n1 + 1)))) by A315, XREAL_1:15;
hence (Sum (mid H₁(D1),(n1 + 1),j)) - (Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A348, XXREAL_0:2; :: thesis:

end;

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

A350: j -' (n1 + 1) = j - (n1 + 1) by A258, XREAL_1:235;
then A351: (j -' (n1 + 1)) + 1 = j - n1 ;
A352: n1 < n1 + 1 by NAT_1:13;
then A353: D1 . n1 < D1 . (n1 + 1) by A241, A266, SEQM_3:def 1;
then consider B being 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 A10, A232, A258, A266, A276, Th14;
A359: len MD1 = (j -' (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A357, JORDAN3:27;
then A360: len MD1 = (j - (n1 + 1)) + 1 by A258, XREAL_1:235;
then A361: ((len MD1) + (n1 + 1)) - 1 = j ;
A362: len MD1 in dom MD1 by FINSEQ_5:6;
then A363: 1 <= len MD1 by FINSEQ_3:27;
A364: ( 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 A365: len MD1 = 1 ; :: thesis:

then A366: upper_bound (divset MD1,(len MD1)) = MD1 . (len MD1) by A362, INTEGRA1:def 5;
A367: upper_bound (divset D1,j) = D1 . j by A232, A245, A277, INTEGRA1:def 5;
lower_bound (divset D1,j) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 5;
hence ( lower_bound (divset MD1,(len MD1)) = lower_bound (divset D1,j) & upper_bound (divset MD1,(len MD1)) = upper_bound (divset D1,j) ) by A261, A264, A354, A357, A360, A362, A365, A366, A367, INTEGRA1:def 5, JORDAN3:27; :: thesis:

end;

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

then (len MD1) - 1 in dom MD1 by A362, INTEGRA1:9;
then A369: (len MD1) - 1 >= 1 by FINSEQ_3:27;
len MD1 <= (len MD1) + 1 by NAT_1:11;
then A370: (len MD1) - 1 <= len MD1 by XREAL_1:22;
upper_bound (divset MD1,(len MD1)) = MD1 . (len MD1) by A362, A368, INTEGRA1:def 5;
then A371: upper_bound (divset MD1,(len MD1)) = D1 . j by A258, A264, A244, A357, A359, A361, A363, JORDAN3:31;
A372: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A359, A350;
lower_bound (divset MD1,(len MD1)) = MD1 . ((len MD1) - 1) by A362, A368, INTEGRA1:def 5;
then lower_bound (divset MD1,(len MD1)) = D1 . (j - 1) by A258, A264, A244, A357, A359, A372, A369, A370, JORDAN3:31;
hence ( lower_bound (divset MD1,(len MD1)) = lower_bound (divset D1,j) & upper_bound (divset MD1,(len MD1)) = upper_bound (divset D1,j) ) by A232, A245, A277, A371, INTEGRA1:def 5; :: thesis:

end;

A373: B c= A

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis:
A374: rng D1 c= A by INTEGRA1:def 2;
D1 . n1 in rng D1 by A241, FUNCT_1:def 5;
then A375: lower_bound A <= D1 . n1 by A374, INTEGRA2:1;
assume A376: x1 in B ; :: thesis:
then reconsider x1 = x1 as Real ;
A377: x1 <= MD1 . (len MD1) by A355, A376, INTEGRA2:1;
D1 . j in rng D1 by A232, FUNCT_1:def 5;
then A378: D1 . j <= upper_bound A by A374, INTEGRA2:1;
D1 . n1 <= x1 by A354, A376, INTEGRA2:1;
then A379: lower_bound A <= x1 by A375, XXREAL_0:2;
MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A258, A278, A264, A244, A357, A359, A350, JORDAN3:31
.= D1 . j ;
then x1 <= upper_bound A by A377, A378, XXREAL_0:2;
hence x1 in A by A379, INTEGRA2:1; :: thesis:

end;

then reconsider g = f | B as Function of B,REAL by FUNCT_2:38;
A380: delta MD1 >= 0 by Th8;
A381: g | B is bounded

proof

consider a being real number such that
A382: for x being set st x in A /\ (dom f) holds
a <= f . x by A1, RFUNCT_1:88;
for x being set st x in B /\ (dom g) holds
a <= g . x

proof

let x be set ; :: thesis:
A383: (dom f) /\ B c= (dom f) /\ A by A373, XBOOLE_1:26;
assume x in B /\ (dom g) ; :: thesis:
then A384: x in dom g by XBOOLE_0:def 4;
then x in (dom f) /\ B by RELAT_1:90;
then a <= f . x by A382, A383;
hence a <= g . x by A384, FUNCT_1:70; :: thesis:

end;

then A385: g | B is bounded_below by RFUNCT_1:88;
consider a being real number such that
A386: for x being set st x in A /\ (dom f) holds
f . x <= a by A1, RFUNCT_1:87;
for x being set st x in B /\ (dom g) holds
g . x <= a

proof

let x be set ; :: thesis:
A387: (dom f) /\ B c= (dom f) /\ A by A373, XBOOLE_1:26;
assume x in B /\ (dom g) ; :: thesis:
then A388: x in dom g by XBOOLE_0:def 4;
then x in (dom f) /\ B by RELAT_1:90;
then a >= f . x by A386, A387;
hence g . x <= a by A388, FUNCT_1:70; :: thesis:

end;

then g | B is bounded_above by RFUNCT_1:87;
hence g | B is bounded by A385; :: thesis:

end;

lower_bound (divset D1,j) <= D . (i + 1) by A233, INTEGRA2:1;
then A389: D1 . (j - 1) <= D . (i + 1) by A232, A245, A277, INTEGRA1:def 5;
A390: (j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A258, XREAL_1:235;
A391: len (upper_volume g,MD1) = len MD1 by INTEGRA1:def 7
.= (j - (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A357, A390, JORDAN3:27 ;
A392: j <= len H₁(D1) by A264, INTEGRA1:def 7;
A393: for k being Nat st 1 <= k & k <= len (upper_volume g,MD1) holds
(upper_volume g,MD1) . k = (mid H₁(D1),(n1 + 1),j) . k

proof

let k be Nat; :: thesis:
assume that
A394: 1 <= k and
A395: k <= len (upper_volume g,MD1) ; :: thesis:
A396: k in Seg (len (upper_volume g,MD1)) by A394, A395, FINSEQ_1:3;
then A397: k in Seg (len MD1) by INTEGRA1:def 7;
then A398: k in dom MD1 by FINSEQ_1:def 3;
k in dom MD1 by A397, FINSEQ_1:def 3;
then A399: (upper_volume g,MD1) . k = (upper_bound (rng (g | (divset MD1,k)))) * (vol (divset MD1,k)) by INTEGRA1:def 7;
consider k2 being Element of NAT such that
A400: n1 + 1 = 1 + k2 ;
A401: 1 <= k + k2 by A394, NAT_1:12;
k <= j - ((n1 + 1) - 1) by A391, A395;
then k + ((n1 + 1) - 1) <= j by XREAL_1:21;
then k + k2 <= len D1 by A264, A400, XXREAL_0:2;
then A402: k + k2 in Seg (len D1) by A401, FINSEQ_1:3;
then A403: k + k2 in dom D1 by FINSEQ_1:def 3;
1 + 1 <= k + k2 by A259, A394, A400, XREAL_1:9;
then A404: 1 < k + k2 by NAT_1:13;
A405: k2 = (n1 + 1) - 1 by A400;
A406: ( 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 A407: k = 1 ; :: thesis:

then upper_bound (divset MD1,k) = MD1 . k by A398, INTEGRA1:def 5;
then A408: upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A357, A391, A394, A395, A396, JORDAN3:31;
lower_bound (divset MD1,k) = D1 . n1 by A354, A398, A407, INTEGRA1:def 5;
hence ( lower_bound (divset D1,(k + k2)) = lower_bound (divset MD1,k) & upper_bound (divset D1,(k + k2)) = upper_bound (divset MD1,k) ) by A405, A404, A403, A407, A408, INTEGRA1:def 5; :: thesis:

end;

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

then upper_bound (divset MD1,k) = MD1 . k by A398, INTEGRA1:def 5;
then A410: upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A357, A391, A394, A395, A396, JORDAN3:31;
A411: k - 1 <= (j - (n1 + 1)) + 1 by A391, A395, XREAL_1:148, XXREAL_0:2;
A412: lower_bound (divset MD1,k) = MD1 . (k - 1) by A398, A409, INTEGRA1:def 5;
A413: k - 1 in dom MD1 by A398, A409, INTEGRA1:9;
then 1 <= k - 1 by FINSEQ_3:27;
then lower_bound (divset MD1,k) = D1 . (((k - 1) + (n1 + 1)) - 1) by A258, A264, A244, A357, A413, A411, A412, JORDAN3:31;
hence ( lower_bound (divset D1,(k + k2)) = lower_bound (divset MD1,k) & upper_bound (divset D1,(k + k2)) = upper_bound (divset MD1,k) ) by A400, A404, A403, A410, INTEGRA1:def 5; :: thesis:

end;

divset MD1,k = [.(lower_bound (divset MD1,k)),(upper_bound (divset MD1,k)).] by INTEGRA1:5;
then A414: divset D1,(k + k2) = divset MD1,k by A406, INTEGRA1:5;
A415: k + k2 in dom D1 by A402, FINSEQ_1:def 3;
A416: (mid H₁(D1),(n1 + 1),j) . k = H₁(D1) . ((k + (n1 + 1)) - 1) by A258, A244, A391, A392, A394, A395, A396, JORDAN3:31
.= (upper_bound (rng (f | (divset D1,(k + k2))))) * (vol (divset D1,(k + k2))) by A400, A415, INTEGRA1:def 7 ;
k in dom MD1 by A397, FINSEQ_1:def 3;
then divset D1,(k + k2) c= B by A414, INTEGRA1:10;
hence (upper_volume g,MD1) . k = (mid H₁(D1),(n1 + 1),j) . k by A399, A416, A414, FUNCT_1:82; :: thesis:

end;

n1 + 1 <= len H₁(D1) by A265, INTEGRA1:def 7;
then len (upper_volume g,MD1) = len (mid H₁(D1),(n1 + 1),j) by A258, A261, A244, A390, A391, A392, JORDAN3:27;
then A417: Sum (upper_volume g,MD1) = Sum (mid H₁(D1),(n1 + 1),j) by A393, FINSEQ_1:18;
A418: n1 < j - 1 by A349, XREAL_1:22;
A419: 1 <= (indx D2,D1,n1) + 1 by A263, NAT_1:13;
A420: len MD1 in dom MD1 by FINSEQ_5:6;
A421: 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 A420, INTEGRA1:def 5; :: thesis:

end;

suppose len MD1 <> 1 ; :: thesis:

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

end;

vol B = (upper_bound B) - (D1 . n1) by A354, INTEGRA1:def 6;
then vol B = (D1 . j) - (D1 . n1) by A232, A245, A277, A355, A364, A421, INTEGRA1:def 5;
then A422: vol B <> 0 by A232, A241, A245, SEQM_3:def 1;
rng f is bounded_below by A1, INTEGRA1:13;
then A423: lower_bound (rng f) <= lower_bound (rng g) by RELAT_1:99, SEQ_4:64;
rng f is bounded_above by A1, INTEGRA1:15;
then upper_bound (rng f) >= upper_bound (rng g) by RELAT_1:99, SEQ_4:65;
then (upper_bound (rng f)) - (lower_bound (rng f)) >= (upper_bound (rng g)) - (lower_bound (rng g)) by A423, XREAL_1:15;
then A424: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A380, XREAL_1:66;
D1 . n1 < D1 . (n1 + 1) by A241, A266, A352, SEQM_3:def 1;
then indx D2,D1,n1 < indx D2,D1,(n1 + 1) by A262, A260, A270, A267, GOBOARD2:18;
then A425: (indx D2,D1,n1) + 1 <= indx D2,D1,(n1 + 1) by NAT_1:13;
then A426: (indx D2,D1,n1) + 1 <= len D2 by A274, XXREAL_0:2;
A427: indx D2,D1,n1 < (indx D2,D1,n1) + 1 by NAT_1:13;
A428: indx D2,D1,(n1 + 1) = (indx D2,D1,n1) + 1

proof

assume indx D2,D1,(n1 + 1) <> (indx D2,D1,n1) + 1 ; :: thesis:
then A429: indx D2,D1,(n1 + 1) > (indx D2,D1,n1) + 1 by A425, XXREAL_0:1;
A430: (indx D2,D1,n1) + 1 in dom D2 by A419, A426, FINSEQ_3:27;
then A431: D2 . ((indx D2,D1,n1) + 1) in rng D2 by FUNCT_1:def 5;

now

per cases by A11, A431, XBOOLE_0:def 3;

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

then consider n2 being Element of NAT such that
A432: n2 in dom D1 and
A433: D2 . ((indx D2,D1,n1) + 1) = D1 . n2 by PARTFUN1:26;
D2 . (indx D2,D1,n1) < D2 . ((indx D2,D1,n1) + 1) by A262, A427, A430, SEQM_3:def 1;
then n1 < n2 by A241, A260, A432, A433, GOBOARD2:18;
then A434: n1 + 1 <= n2 by NAT_1:13;
D1 . n2 < D1 . (n1 + 1) by A270, A267, A429, A430, A433, SEQM_3:def 1;
hence contradiction by A266, A432, A434, GOBOARD2:18; :: thesis:

end;

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

A436: D . i <= upper_bound (divset D1,n1) by A242, INTEGRA2:1;
A437: 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 5; :: thesis:

end;

suppose n1 <> 1 ; :: thesis:

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

end;

consider n2 being Element of NAT such that
A438: n2 in dom D and
A439: D2 . ((indx D2,D1,n1) + 1) = D . n2 by A435, PARTFUN1:26;
D1 . n1 < D . n2 by A262, A260, A427, A430, A439, SEQM_3:def 1;
then D . i < D . n2 by A436, A437, XXREAL_0:2;
then i < n2 by A236, A438, GOBOARD2:18;
then A440: i + 1 <= n2 by NAT_1:13;
(n1 + 1) + 1 <= j by A349, NAT_1:13;
then A441: n1 + 1 <= j - 1 by XREAL_1:21;
j - 1 in dom D1 by A232, A245, A277, INTEGRA1:9;
then A442: D1 . (n1 + 1) <= D1 . (j - 1) by A266, A441, GOBOARD2:18;
A443: lower_bound (divset D1,j) <= D . (i + 1) by A233, INTEGRA2:1;
lower_bound (divset D1,j) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 5;
then A444: D1 . (n1 + 1) <= D . (i + 1) by A442, A443, XXREAL_0:2;
D . n2 < D1 . (n1 + 1) by A270, A267, A429, A430, A439, SEQM_3:def 1;
then D . n2 < D . (i + 1) by A444, XXREAL_0:2;
hence contradiction by A231, A438, A440, GOBOARD2:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A445: len MD2 = ((indx D2,D1,j) -' (indx D2,D1,(n1 + 1))) + 1 by A275, A271, A274, A238, A239, A358, JORDAN3:27;
then A446: len MD2 = ((indx D2,D1,j) - (indx D2,D1,(n1 + 1))) + 1 by A275, XREAL_1:235;
then A447: len (upper_volume g,MD2) = ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A428, INTEGRA1:def 7;
for x1 being set st x1 in (rng MD1) \/ {(D . (i + 1))} holds
x1 in rng MD2

proof

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

now

per cases by A448, XBOOLE_0:def 3;

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

end;

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

then A463: x1 = D . (i + 1) by TARSKI:def 1;
reconsider j1 = j - 1 as Element of NAT by A232, A245, A277, INTEGRA1:9;
A464: rng D c= rng D2 by A9, INTEGRA1:def 20;
D . (i + 1) in rng D by A231, FUNCT_1:def 5;
then consider k being Element of NAT such that
A465: k in dom D2 and
A466: x1 = D2 . k by A463, A464, PARTFUN1:26;
D . (i + 1) <= upper_bound (divset D1,j) by A233, INTEGRA2:1;
then x1 <= D1 . j by A232, A245, A277, A463, INTEGRA1:def 5;
then A467: D2 . k <= D2 . (indx D2,D1,j) by A10, A232, A466, INTEGRA1:def 21;
n1 < j1 by A349, XREAL_1:22;
then A468: n1 + 1 <= j1 by NAT_1:13;
j - 1 in dom D1 by A232, A245, A277, INTEGRA1:9;
then A469: D1 . (n1 + 1) <= D1 . (j - 1) by A266, A468, GOBOARD2:18;
lower_bound (divset D1,j) <= D . (i + 1) by A233, INTEGRA2:1;
then D1 . (j - 1) <= x1 by A232, A245, A277, A463, INTEGRA1:def 5;
then D2 . (indx D2,D1,(n1 + 1)) <= D2 . k by A267, A466, A469, XXREAL_0:2;
hence x1 in rng MD2 by A270, A237, A358, A465, A466, A467, Th16; :: thesis:

end;

hence x1 in rng MD2 ; :: thesis:

end;

then A470: (rng MD1) \/ {(D . (i + 1))} c= rng MD2 by TARSKI:def 3;
rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:34;
then A471: 1 <= len MD2 by FINSEQ_3:27;
A472: ((len MD2) - 1) + (indx D2,D1,(n1 + 1)) = indx D2,D1,j by A446;
for x1 being set st x1 in rng MD2 holds
x1 in (rng MD1) \/ {(D . (i + 1))}

proof

let x1 be set ; :: thesis:
assume A473: x1 in rng MD2 ; :: thesis:
then reconsider x1 = x1 as Real ;
A474: MD2 . 1 <= x1 by A473, Th15;
A475: MD2 . (len MD2) = D2 . (indx D2,D1,j) by A275, A271, A239, A358, A471, A445, A472, JORDAN3:31;
A476: rng MD2 c= rng D2 by A358, JORDAN3:28;
A477: MD2 . 1 = D2 . (indx D2,D1,(n1 + 1)) by A271, A274, A238, A239, A358, JORDAN3:27;
A478: x1 <= MD2 . (len MD2) by A473, Th15;
then A479: x1 <= D1 . j by A234, A275, A271, A239, A358, A471, A445, A472, JORDAN3:31;

now

per cases by A11, A473, A476, XBOOLE_0:def 3;

suppose x1 in rng D1 ; :: thesis:

then consider k being Element of NAT such that
A480: k in dom D1 and
A481: D1 . k = x1 by PARTFUN1:26;
A482: n1 + 1 <= k by A266, A267, A474, A477, A480, A481, SEQM_3:def 1;
then A483: 1 <= k - n1 by XREAL_1:21;
n1 <= n1 + 1 by NAT_1:11;
then consider n being Nat such that
A484: k = n1 + n by A482, NAT_1:10, XXREAL_0:2;
A485: k <= j by A232, A234, A478, A475, A480, A481, SEQM_3:def 1;
then A486: k - n1 <= j - n1 by XREAL_1:11;
A487: 1 <= k - n1 by A482, XREAL_1:21;
A488: (j - (n1 + 1)) + 1 = j - n1 ;
k - n1 <= len MD1 by A359, A351, A485, XREAL_1:11;
then n in dom MD1 by A487, A484, FINSEQ_3:27;
then A489: MD1 . n in rng MD1 by FUNCT_1:def 5;
n in NAT by ORDINAL1:def 13;
then MD1 . n = D1 . (((k - n1) - 1) + (n1 + 1)) by A258, A264, A244, A357, A483, A486, A488, A484, JORDAN3:31
.= D1 . k ;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by A481, A489, XBOOLE_0:def 3; :: thesis:

end;

suppose x1 in rng D ; :: thesis:

then consider n being Element of NAT such that
A490: n in dom D and
A491: D . n = x1 by PARTFUN1:26;
A492: not i + 1 < n

proof

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

proof

per cases ;

suppose j = 1 ; :: thesis:

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

end;

suppose j <> 1 ; :: thesis:

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

end;

consider y1 being Real such that
A494: y1 = D . (i + 1) ;
A495: D . n in rng D by A490, FUNCT_1:def 5;
assume i + 1 < n ; :: thesis:
then A496: D . (i + 1) < D . n by A231, A490, SEQM_3:def 1;
lower_bound (divset D1,j) <= D . (i + 1) by A233, INTEGRA2:1;
then lower_bound (divset D1,j) <= D . n by A496, XXREAL_0:2;
then D . n in divset D1,j by A479, A491, A493, INTEGRA2:1;
then A497: x1 in (rng D) /\ (divset D1,j) by A491, A495, XBOOLE_0:def 4;
D . (i + 1) in rng D by A231, FUNCT_1:def 5;
then y1 in (rng D) /\ (divset D1,j) by A233, A494, XBOOLE_0:def 4;
hence contradiction by A8, A232, A491, A496, A497, A494, Th4; :: thesis:

end;

A498: 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 5; :: thesis:

end;

suppose n1 <> 1 ; :: thesis:

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

end;

D . i <= upper_bound (divset D1,n1) by A242, INTEGRA2:1;
then D . i < D1 . (n1 + 1) by A353, A498, XXREAL_0:2;
then D . i < D . n by A267, A474, A477, A491, XXREAL_0:2;
then i < n by A236, A490, GOBOARD2:18;
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 A491, A492, 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))} by TARSKI:def 3;
then A499: rng MD2 = (rng MD1) \/ {(D . (i + 1))} by A470, XBOOLE_0:def 10;
delta MD1 = max (rng (upper_volume (chi B,B),MD1)) by INTEGRA1:def 19;
then delta MD1 in rng (upper_volume (chi B,B),MD1) by XXREAL_2:def 8;
then consider k being Element of NAT such that
A500: k in dom (upper_volume (chi B,B),MD1) and
A501: (upper_volume (chi B,B),MD1) . k = delta MD1 by PARTFUN1:26;
A502: k in Seg (len (upper_volume (chi B,B),MD1)) by A500, FINSEQ_1:def 3;
then A503: k in Seg (len MD1) by INTEGRA1:def 7;
then A504: k in dom MD1 by FINSEQ_1:def 3;
A505: k <= len MD1 by A503, FINSEQ_1:3;
then k + n1 <= j by A359, A351, XREAL_1:21;
then A506: k + n1 <= len D1 by A264, XXREAL_0:2;
A507: 1 <= k by A502, FINSEQ_1:3;
A508: n1 + 1 > 1 by A277, NAT_1:13;
then n1 > 1 - 1 by XREAL_1:21;
then A509: k < k + n1 by XREAL_1:31;
then 1 < k + n1 by A507, XXREAL_0:2;
then A510: k + n1 in dom D1 by A506, FINSEQ_3:27;
( 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 A511: k = 1 ; :: thesis:

then upper_bound (divset MD1,k) = MD1 . k by A504, INTEGRA1:def 5;
then A512: upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A357, A359, A507, A505, JORDAN3:31;
lower_bound (divset D1,(k + n1)) = D1 . ((k + n1) - 1) by A507, A509, A510, INTEGRA1:def 5;
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, A508, A504, A510, A511, A512, INTEGRA1:def 5; :: thesis:

end;

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

then upper_bound (divset MD1,k) = MD1 . k by A504, INTEGRA1:def 5;
then A514: upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A357, A359, A507, A505, JORDAN3:31;
A515: lower_bound (divset MD1,k) = MD1 . (k - 1) by A504, A513, INTEGRA1:def 5;
A516: k - 1 in dom MD1 by A504, A513, INTEGRA1:9;
then A517: k - 1 <= len MD1 by FINSEQ_3:27;
1 <= k - 1 by A516, FINSEQ_3:27;
then lower_bound (divset MD1,k) = D1 . (((k - 1) + (n1 + 1)) - 1) by A258, A264, A244, A357, A359, A516, A517, A515, JORDAN3:31;
hence ( lower_bound (divset MD1,k) = lower_bound (divset D1,(k + n1)) & upper_bound (divset MD1,k) = upper_bound (divset D1,(k + n1)) ) by A507, A509, A510, A514, INTEGRA1:def 5; :: thesis:

end;

then divset MD1,k = [.(lower_bound (divset D1,(k + n1))),(upper_bound (divset D1,(k + n1))).] by INTEGRA1:5;
then A518: divset MD1,k = divset D1,(k + n1) by INTEGRA1:5;
k + n1 in Seg (len D1) by A510, FINSEQ_1:def 3;
then k + n1 in Seg (len (upper_volume (chi A,A),D1)) by INTEGRA1:def 7;
then A519: k + n1 in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
k in dom MD1 by A503, FINSEQ_1:def 3;
then delta MD1 = vol (divset MD1,k) by A501, INTEGRA1:22;
then delta MD1 = (upper_volume (chi A,A),D1) . (k + n1) by A510, A518, INTEGRA1:22;
then delta MD1 in rng (upper_volume (chi A,A),D1) by A519, FUNCT_1:def 5;
then delta MD1 <= max (rng (upper_volume (chi A,A),D1)) by XXREAL_2:def 8;
then A520: delta MD1 <= delta D1 by INTEGRA1:def 19;
A521: D . (i + 1) <= upper_bound (divset D1,j) by A233, INTEGRA2:1;
lower_bound (divset D1,j) <= D . (i + 1) by A233, INTEGRA2:1;
then A522: D . (i + 1) in divset MD1,(len MD1) by A364, A521, INTEGRA2:1;
j - 1 in dom D1 by A232, A245, A277, INTEGRA1:9;
then D1 . n1 < D1 . (j - 1) by A241, A418, SEQM_3:def 1;
then D . (i + 1) > lower_bound B by A354, A389, XXREAL_0:2;
then (Sum (upper_volume g,MD1)) - (Sum (upper_volume g,MD2)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A356, A381, A499, A522, A422, Th13;
then A523: (Sum (upper_volume g,MD1)) - (Sum (upper_volume g,MD2)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A424, XXREAL_0:2;
A524: indx D2,D1,j <= len H₁(D2) by A239, INTEGRA1:def 7;
A525: (indx D2,D1,n1) + 1 <= indx D2,D1,j by A275, A425, XXREAL_0:2;
A526: for k being Nat st 1 <= k & k <= len (upper_volume g,MD2) holds
(upper_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
A527: 1 <= k and
A528: k <= len (upper_volume g,MD2) ; :: thesis:
A529: k in Seg (len (upper_volume g,MD2)) by A527, A528, FINSEQ_1:3;
then A530: (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k = H₁(D2) . ((k + ((indx D2,D1,n1) + 1)) - 1) by A419, A447, A524, A525, A527, A528, JORDAN3:31;
A531: k in Seg (len MD2) by A529, INTEGRA1:def 7;
then k in dom MD2 by FINSEQ_1:def 3;
then A532: (upper_volume g,MD2) . k = (upper_bound (rng (g | (divset MD2,k)))) * (vol (divset MD2,k)) by INTEGRA1:def 7;
1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
then 1 + 1 <= k + ((indx D2,D1,n1) + 1) by A527, XREAL_1:9;
then A533: 1 <= (k + ((indx D2,D1,n1) + 1)) - 1 by XREAL_1:21;
consider k2 being Element of NAT such that
A534: (indx D2,D1,n1) + 1 = 1 + k2 ;
k <= (indx D2,D1,j) - (((indx D2,D1,n1) + 1) - 1) by A446, A428, A528, INTEGRA1:def 7;
then k + (((indx D2,D1,n1) + 1) - 1) <= indx D2,D1,j by XREAL_1:21;
then (k + ((indx D2,D1,n1) + 1)) - 1 <= len H₁(D2) by A524, XXREAL_0:2;
then k + k2 in Seg (len H₁(D2)) by A533, A534, FINSEQ_1:3;
then A535: k + k2 in Seg (len D2) by INTEGRA1:def 7;
then k + k2 in dom D2 by FINSEQ_1:def 3;
then A536: (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k = (upper_bound (rng (f | (divset D2,(k + k2))))) * (vol (divset D2,(k + k2))) by A530, A534, INTEGRA1:def 7;
A537: ( 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 A263, A527, A534, XREAL_1:9;
then A538: k + k2 > 1 by NAT_1:13;
A539: k in dom MD2 by A531, FINSEQ_1:def 3;
A540: k + k2 in dom D2 by A535, FINSEQ_1:def 3;

per cases ;

suppose A541: k = 1 ; :: thesis:

then A542: upper_bound (divset D2,(k + k2)) = D2 . (1 + k2) by A538, A540, INTEGRA1:def 5;
A543: lower_bound (divset MD2,k) = lower_bound B by A539, A541, INTEGRA1:def 5;
upper_bound (divset MD2,k) = MD2 . k by A539, A541, INTEGRA1:def 5;
then A544: upper_bound (divset MD2,k) = D2 . ((1 + (indx D2,D1,(n1 + 1))) - 1) by A275, A239, A358, A419, A428, A447, A528, A541, JORDAN3:31
.= D1 . (n1 + 1) by A10, A266, INTEGRA1:def 21 ;
lower_bound (divset D2,(k + k2)) = D2 . ((1 + k2) - 1) by A538, A540, A541, INTEGRA1:def 5;
hence ( lower_bound (divset MD2,k) = lower_bound (divset D2,(k + k2)) & upper_bound (divset MD2,k) = upper_bound (divset D2,(k + k2)) ) by A10, A241, A266, A354, A428, A534, A543, A544, A542, INTEGRA1:def 21; :: thesis:

end;

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

then upper_bound (divset MD2,k) = MD2 . k by A539, INTEGRA1:def 5;
then A546: upper_bound (divset MD2,k) = D2 . ((k + ((indx D2,D1,n1) + 1)) - 1) by A275, A239, A358, A419, A428, A447, A527, A528, A529, JORDAN3:31;
A547: k - 1 <= ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A447, A528, XREAL_1:148, XXREAL_0:2;
A548: lower_bound (divset MD2,k) = MD2 . (k - 1) by A539, A545, INTEGRA1:def 5;
A549: k - 1 in dom MD2 by A539, A545, INTEGRA1:9;
then 1 <= k - 1 by FINSEQ_3:27;
then lower_bound (divset MD2,k) = D2 . (((k - 1) + ((indx D2,D1,n1) + 1)) - 1) by A275, A239, A358, A419, A428, A549, A547, A548, JORDAN3:31;
hence ( lower_bound (divset MD2,k) = lower_bound (divset D2,(k + k2)) & upper_bound (divset MD2,k) = upper_bound (divset D2,(k + k2)) ) by A534, A538, A540, A546, INTEGRA1:def 5; :: thesis:

end;

divset MD2,k = [.(lower_bound (divset MD2,k)),(upper_bound (divset MD2,k)).] by INTEGRA1:5;
then A550: divset MD2,k = divset D2,(k + k2) by A537, INTEGRA1:5;
k in dom MD2 by A531, FINSEQ_1:def 3;
then divset D2,(k + k2) c= B by A550, INTEGRA1:10;
hence (upper_volume g,MD2) . k = (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k by A532, A536, A550, FUNCT_1:82; :: thesis:

end;

(indx D2,D1,n1) + 1 <= len H₁(D2) by A426, 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 A238, A419, A524, A525, JORDAN3:27;
then len (upper_volume g,MD2) = len (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) by A275, A425, A447, XREAL_1:235, XXREAL_0:2;
then A551: Sum (upper_volume g,MD2) = Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) by A526, FINSEQ_1:18;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:50;
then ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A520, XREAL_1:66;
hence (Sum (mid H₁(D1),(n1 + 1),j)) - (Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A523, A551, A417, XXREAL_0:2; :: thesis:

end;

then A552: (H₂(D1,n1) - H₂(D2, indx D2,D1,n1)) + ((Sum (mid H₁(D1),(n1 + 1),j)) - (Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,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:9;
n1 < n1 + 1 by NAT_1:13;
then D1 . n1 < D1 . (n1 + 1) by A241, A266, SEQM_3:def 1;
then indx D2,D1,n1 < indx D2,D1,(n1 + 1) by A262, A260, A270, A267, GOBOARD2:18;
then A553: indx D2,D1,n1 < indx D2,D1,j by A275, XXREAL_0:2;
indx D2,D1,n1 in Seg (len D2) by A262, 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 22
.= Sum (mid H₁(D2),1,(indx D2,D1,n1)) by A263, JORDAN3:25 ;
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:105
.= Sum (mid H₁(D2),1,(indx D2,D1,j)) by A263, A553, A240, INTEGRA2:4
.= Sum (H₁(D2) | (indx D2,D1,j)) by A238, JORDAN3:25 ;
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 A273, INTEGRA1:def 22;
then (H₂(D1,n1) - H₂(D2, indx D2,D1,n1)) + ((Sum (mid H₁(D1),(n1 + 1),j)) - (Sum (mid H₁(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)))) = H₂(D1,j) - H₂(D2, indx D2,D1,j) by A272;
hence ex j being Element of NAT st
( j in dom D1 & D . (i + 1) in divset D1,j & H₂(D1,j) - H₂(D2, indx D2,D1,j) <= ((i + 1) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A232, A233, A552; :: thesis:

end;

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

end;

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

end;

A554: len D1 in dom D1 by FINSEQ_5:6;
then D1 . (len D1) = D2 . (indx D2,D1,(len D1)) by A10, INTEGRA1:def 21;
then upper_bound A = D2 . (indx D2,D1,(len D1)) by INTEGRA1:def 2;
then A555: 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
A556: j in dom D1 and
A557: D . (len D) in divset D1,j and
A558: H₂(D1,j) - H₂(D2, indx D2,D1,j) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A13;
A559: j = len D1

proof

j in Seg (len D1) by A556, FINSEQ_1:def 3;
then A560: j <= len D1 by FINSEQ_1:3;
assume j <> len D1 ; :: thesis:
then j < len D1 by A560, XXREAL_0:1;
then D1 . j < D1 . (len D1) by A556, A554, SEQM_3:def 1;
then A561: D1 . j < upper_bound A by INTEGRA1:def 2;
A562: 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 A556, A561, INTEGRA1:def 5; :: thesis:

end;

suppose j <> 1 ; :: thesis:

hence upper_bound (divset D1,j) < upper_bound A by A556, A561, INTEGRA1:def 5; :: thesis:

end;

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

end;

indx D2,D1,(len D1) in dom D2 by A10, A554, INTEGRA1:def 21;
then indx D2,D1,(len D1) = len D2 by A12, A555, GOBOARD2:19;
then (upper_sum f,D1) - H₂(D2, len D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A558, A559, INTEGRA1:44;
hence (upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by INTEGRA1:44; :: thesis:

end;

hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A9, A10, A11; :: thesis:

end;

assume A563: delta T is convergent_to_0 ; :: thesis:
then A564: delta T is convergent by FDIFF_1:def 1;
A565: lim (delta T) = 0 by A563, FDIFF_1:def 1;
assume A566: vol A <> 0 ; :: thesis:
A567: delta T is non-empty by A563, FDIFF_1:def 1;
A568: for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )

proof

let e be Real; :: thesis:
assume e > 0 ; :: thesis:
then consider n being Element of NAT such that
A569: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < e by A564, A565, SEQ_2:def 7;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then abs (((delta T) . m) - 0 ) < e by A569;
then A570: ((delta T) . m) + (abs (((delta T) . m) - 0 )) < e + (abs (((delta T) . m) - 0 )) by ABSVALUE:11, XREAL_1:10;
reconsider D = T . m as Division of A ;
A571: (delta T) . m = delta (T . m) by INTEGRA2:def 3;
delta (T . m) = max (rng (upper_volume (chi A,A),(T . m))) by INTEGRA1:def 19;
then delta (T . m) in rng (upper_volume (chi A,A),(T . m)) by XXREAL_2:def 8;
then consider i being Element of NAT such that
A572: i in dom (upper_volume (chi A,A),(T . m)) and
A573: delta (T . m) = (upper_volume (chi A,A),(T . m)) . i by PARTFUN1:26;
i in Seg (len (upper_volume (chi A,A),(T . m))) by A572, FINSEQ_1:def 3;
then i in Seg (len D) by INTEGRA1:def 7;
then i in dom D by FINSEQ_1:def 3;
then A574: delta (T . m) = vol (divset (T . m),i) by A573, INTEGRA1:22;
(delta T) . m <> 0 by A567, SEQ_1:7;
hence ( 0 < (delta T) . m & (delta T) . m < e ) by A570, A571, A574, INTEGRA1:11, XREAL_1:8; :: thesis:

end;

A575: for e being real number st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((upper_sum f,T) . m) - (upper_integral f)) < e

proof

not dom (upper_sum_set f) is empty by INTEGRA1:def 11;
then A576: not rng (upper_sum_set f) is empty by RELAT_1:65;
let e be real number ; :: thesis:
assume A577: e > 0 ; :: thesis:
then A578: e / 2 > 0 by XREAL_1:141;
reconsider e = e as Real by XREAL_0:def 1;
A579: rng (upper_sum_set f) is bounded_below by A1, INTEGRA2:35;
upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 15;
then consider y being real number such that
A580: y in rng (upper_sum_set f) and
A581: (upper_integral f) + (e / 2) > y by A578, A579, A576, SEQ_4:def 5;
ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

proof

consider D3 being Element of divs A such that
A582: D3 in dom (upper_sum_set f) and
A583: y = (upper_sum_set f) . D3 by A580, PARTFUN1:26;
reconsider D3 = D3 as Division of A by INTEGRA1:def 3;
A584: len D3 in Seg (len D3) by FINSEQ_1:5;
then 1 <= len D3 by FINSEQ_1:3;
then 1 in Seg (len D3) by FINSEQ_1:3;
then A585: 1 in dom D3 by FINSEQ_1:def 3;

per cases ;

suppose A586: D3 . 1 <> lower_bound A ; :: thesis:

D3 . 1 in A by A585, INTEGRA1:8;
then lower_bound A <= D3 . 1 by INTEGRA2:1;
then D3 . 1 > lower_bound A by A586, XXREAL_0:1;
hence ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A582, A583; :: thesis:

end;

suppose A587: D3 . 1 = lower_bound A ; :: thesis:

ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )

proof

proof

let i be Nat; :: thesis:
assume that
A604: 1 <= i and
A605: i <= len (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) ; :: thesis:
A606: 1 <= i + 1 by NAT_1:12;
i + 1 <= len D3 by A602, A605, XREAL_1:21;
then A607: i + 1 in Seg (len D3) by A606, FINSEQ_1:3;
then A608: i + 1 in dom D3 by FINSEQ_1:def 3;
A609: divset D3,(i + 1) = divset D,i

proof

A610: i + 1 in dom D3 by A607, FINSEQ_1:def 3;
A611: 1 <> i + 1 by A604, NAT_1:13;
then A612: upper_bound (divset D3,(i + 1)) = D3 . (i + 1) by A610, INTEGRA1:def 5;
A613: i in dom D by A593, A602, A604, A605, FINSEQ_3:27;
then A614: D . i = D3 . (i + 1) by A592, RFINSEQ:def 2;
A615: lower_bound (divset D3,(i + 1)) = D3 . ((i + 1) - 1) by A611, A610, INTEGRA1:def 5;

per cases ;

suppose A616: i = 1 ; :: thesis:

then A617: upper_bound (divset D,i) = D . i by A613, INTEGRA1:def 5;
A618: lower_bound (divset D,i) = lower_bound A by A613, A616, INTEGRA1:def 5;
divset D3,(i + 1) = [.(lower_bound A),(D . i).] by A587, A612, A615, A614, A616, INTEGRA1:5;
hence divset D3,(i + 1) = divset D,i by A618, A617, INTEGRA1:5; :: thesis:

end;

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

then i - 1 in dom D by A613, INTEGRA1:9;
then A620: D . (i - 1) = D3 . ((i - 1) + 1) by A592, RFINSEQ:def 2
.= D3 . i ;
A621: upper_bound (divset D,i) = D . i by A613, A619, INTEGRA1:def 5;
lower_bound (divset D,i) = D . (i - 1) by A613, A619, INTEGRA1:def 5;
then divset D3,(i + 1) = [.(lower_bound (divset D,i)),(upper_bound (divset D,i)).] by A612, A615, A614, A621, A620, INTEGRA1:5;
hence divset D3,(i + 1) = divset D,i by INTEGRA1:5; :: thesis:

end;

i <= (len (upper_volume f,D3)) - 1 by A602, A605, INTEGRA1:def 7;
then A622: i <= ((len (upper_volume f,D3)) - 2) + 1 ;
i in NAT by ORDINAL1:def 13;
then (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_volume f,D3) . ((i + 2) - 1) by A601, A604, A622, JORDAN3:31
.= (upper_volume f,D3) . (i + 1) ;
then A623: (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_bound (rng (f | (divset D3,(i + 1))))) * (vol (divset D3,(i + 1))) by A608, INTEGRA1:def 7;
i in Seg (len D) by A593, A602, A604, A605, FINSEQ_1:3;
then i in dom D by FINSEQ_1:def 3;
hence (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_volume f,D) . i by A623, A609, INTEGRA1:def 7; :: thesis:

end;

end;

hence ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis:

end;

then consider D being Division of A such that
A632: D in dom (upper_sum_set f) and
A633: y = (upper_sum_set f) . D and
A634: D . 1 > lower_bound A ;
deffunc H₁( Nat) -> Element of REAL = vol (divset D,$1);
set p = len D;
set H = upper_bound (rng f);
set h = lower_bound (rng f);
consider v being FinSequence of REAL such that
A635: ( len v = len D & ( for j being Nat st j in dom v holds
v . j = H₁(j) ) ) from FINSEQ_2:sch 1();
A636: 2 * (len D) > 0 by XREAL_1:131;
consider v1 being non-decreasing FinSequence of REAL such that
A637: v,v1 are_fiberwise_equipotent by INTEGRA2:3;
defpred S₁[ Nat] means ( $1 in dom v1 & v1 . $1 > 0 );
A638: dom v = Seg (len D) by A635, FINSEQ_1:def 3;
A639: ex k being Nat st S₁[k]

proof

consider H being Function such that
dom H = dom v and
rng H = dom v1 and
H is one-to-one and
A640: v = v1 * H by A637, CLASSES1:85;
consider k being Element of NAT such that
A641: k in dom D and
A642: vol (divset D,k) > 0 by A566, Th1;
A643: dom D = Seg (len D) by FINSEQ_1:def 3;
then H . k in dom v1 by A638, A640, A641, FUNCT_1:21;
then reconsider Hk = H . k as Element of NAT ;
v . k > 0 by A635, A638, A641, A642, A643;
then S₁[Hk] by A638, A640, A641, A643, FUNCT_1:21, FUNCT_1:22;
hence ex k being Nat st S₁[k] ; :: thesis:

end;

consider k being Nat such that
A644: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A639);
A645: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:50;
then A646: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A636, XREAL_1:131;
min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) > 0

proof

per cases by XXREAL_0:15;

suppose min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) = v1 . k ; :: thesis:

hence min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) > 0 by A644; :: thesis:

end;

suppose min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) = e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) ; :: thesis:

hence min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) > 0 by A577, A646, XREAL_1:141; :: thesis:

end;

then consider n being Element of NAT such that
A647: for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) ) by A568;
take n ; :: thesis:
A648: y = upper_sum f,D by A632, A633, INTEGRA1:def 11;
for m being Element of NAT st n <= m holds
abs (((upper_sum f,T) . m) - (upper_integral f)) < e

proof

A649: v1 . 1 > 0

proof

A650: for n1 being Element of NAT st n1 in dom D holds
vol (divset D,n1) > 0

proof

let n1 be Element of NAT ; :: thesis:
assume A651: n1 in dom D ; :: thesis:
then A652: 1 <= n1 by FINSEQ_3:27;

per cases by A652, XXREAL_0:1;

suppose A653: n1 = 1 ; :: thesis:

then A654: upper_bound (divset D,n1) = D . n1 by A651, INTEGRA1:def 5;
lower_bound (divset D,n1) = lower_bound A by A651, A653, INTEGRA1:def 5;
then vol (divset D,n1) = (D . n1) - (lower_bound A) by A654, INTEGRA1:def 6;
hence vol (divset D,n1) > 0 by A634, A653, XREAL_1:52; :: thesis:

end;

suppose A655: n1 > 1 ; :: thesis:

then A656: upper_bound (divset D,n1) = D . n1 by A651, INTEGRA1:def 5;
lower_bound (divset D,n1) = D . (n1 - 1) by A651, A655, INTEGRA1:def 5;
then A657: vol (divset D,n1) = (D . n1) - (D . (n1 - 1)) by A656, INTEGRA1:def 6;
n1 < n1 + 1 by XREAL_1:31;
then A658: n1 - 1 < n1 by XREAL_1:21;
n1 - 1 in dom D by A651, A655, INTEGRA1:9;
then D . (n1 - 1) < D . n1 by A651, A658, SEQM_3:def 1;
hence vol (divset D,n1) > 0 by A657, XREAL_1:52; :: thesis:

end;

A659: k <= len v1 by A644, FINSEQ_3:27;
1 <= k by A644, FINSEQ_3:27;
then 1 <= len v1 by A659, XXREAL_0:2;
then 1 in dom v1 by FINSEQ_3:27;
then A660: v1 . 1 in rng v1 by FUNCT_1:def 5;
rng v = rng v1 by A637, CLASSES1:83;
then consider n1 being Element of NAT such that
A661: n1 in dom v and
A662: v1 . 1 = v . n1 by A660, PARTFUN1:26;
n1 in Seg (len D) by A635, A661, FINSEQ_1:def 3;
then A663: n1 in dom D by FINSEQ_1:def 3;
v1 . 1 = vol (divset D,n1) by A635, A661, A662;
hence v1 . 1 > 0 by A650, A663; :: thesis:

end;

A664: v1 . k = min (rng (upper_volume (chi A,A),D))

proof

A665: k = 1

proof

len v1 = len v by A637, RFINSEQ:16;
then k in Seg (len v) by A644, FINSEQ_1:def 3;
then A666: 1 <= k by FINSEQ_1:3;
k in Seg (len v1) by A644, FINSEQ_1:def 3;
then k <= len v1 by FINSEQ_1:3;
then 1 <= len v1 by A666, XXREAL_0:2;
then A667: 1 in dom v1 by FINSEQ_3:27;
assume k <> 1 ; :: thesis:
then k > 1 by A666, XXREAL_0:1;
hence contradiction by A644, A649, A667; :: thesis:

end;

A668: rng v = rng v1 by A637, CLASSES1:83;
v1 . k in rng (upper_volume (chi A,A),D)

proof

v1 . k in rng v by A644, A668, FUNCT_1:def 5;
then consider k2 being Element of NAT such that
A669: k2 in dom v and
A670: v1 . k = v . k2 by PARTFUN1:26;
A671: k2 in Seg (len D) by A635, A669, FINSEQ_1:def 3;
then A672: k2 in dom D by FINSEQ_1:def 3;
k2 in Seg (len (upper_volume (chi A,A),D)) by A671, INTEGRA1:def 7;
then A673: k2 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
v1 . k = vol (divset D,k2) by A635, A669, A670;
then v1 . k = (upper_volume (chi A,A),D) . k2 by A672, INTEGRA1:22;
hence v1 . k in rng (upper_volume (chi A,A),D) by A673, FUNCT_1:def 5; :: thesis:

end;

end;

end;

hence for m being Element of NAT st n <= m holds
abs (((upper_sum f,T) . m) - (upper_integral f)) < e ; :: thesis:

end;

hence upper_sum f,T is convergent by SEQ_2:def 6; :: thesis:
hence lim (upper_sum f,T) = upper_integral f by A575, SEQ_2:def 7; :: thesis: