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 that
A1: f | A is bounded and
A2: delta T is convergent_to_0 and
A3: vol A <> 0 ; :: thesis:
A4: ( delta T is non-zero & delta T is convergent & lim (delta T) = 0 ) by A2, FDIFF_1:def 1;
A5: 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
A6: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0 ) < e by A4, SEQ_2:def 7;
for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )

proof

let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A7: abs (((delta T) . m) - 0 ) < e by A6;
((delta T) . m) - 0 <= abs (((delta T) . m) - 0 ) by ABSVALUE:11;
then A8: ((delta T) . m) + (abs (((delta T) . m) - 0 )) < e + (abs (((delta T) . m) - 0 )) by A7, XREAL_1:10;
A9: (delta T) . m <> 0 by A4, SEQ_1:7;
A10: (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
A11: ( i in dom (upper_volume (chi A,A),(T . m)) & delta (T . m) = (upper_volume (chi A,A),(T . m)) . i ) by PARTFUN1:26;
A12: i in Seg (len (upper_volume (chi A,A),(T . m))) by A11, FINSEQ_1:def 3;
consider D being Division of A such that
A13: D = T . m by INTEGRA1:def 3;
i in Seg (len D) by A12, A13, INTEGRA1:def 7;
then i in dom D by FINSEQ_1:def 3;
then delta (T . m) = vol (divset (T . m),i) by A11, A13, INTEGRA1:22;
hence ( 0 < (delta T) . m & (delta T) . m < e ) by A8, A9, A10, INTEGRA1:11, XREAL_1:8; :: thesis:

end;

hence 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 ) ; :: thesis:

end;

A14: 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) )

proof

let D, D1 be Division of A; :: thesis:
consider D2 being Division of A such that
A15: ( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) ) by Th3;
A16: f | A is bounded_below by A1;
then A17: (lower_sum f,D2) - (lower_sum f,D) >= 0 by A15, INTEGRA1:48, XREAL_1:50;
(lower_sum f,D2) - (lower_sum f,D1) >= 0 by A15, A16, INTEGRA1:48, XREAL_1:50;
hence 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 A15, A17; :: thesis:

end;

A18: 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 A19: 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
A20: ( 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 A14;
(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, Nat) -> Element of REAL = (PartSums (lower_volume f,$1)) . $2;
deffunc H₂( Division of A) -> FinSequence of REAL = lower_volume f,$1;
A21: 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

let i be Element of NAT ; :: thesis:
assume A22: i in dom D ; :: thesis:
A23: 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 A24: i in dom D ; :: thesis:
assume A25: ( j in dom D1 & D . i in divset D1,j ) ; :: thesis:
assume j < 2 ; :: thesis:
then j < 1 + 1 ;
then A26: j <= 1 by NAT_1:13;
A27: ( lower_bound (divset D1,j) <= D . i & D . i <= upper_bound (divset D1,j) ) by A25, INTEGRA2:1;
j in Seg (len D1) by A25, FINSEQ_1:def 3;
then j >= 1 by FINSEQ_1:3;
then j = 1 by A26, XXREAL_0:1;
then A28: ( lower_bound (divset D1,j) = lower_bound A & upper_bound (divset D1,j) = D1 . j ) by A25, INTEGRA1:def 5;
delta D1 >= min (rng (upper_volume (chi A,A),D))

proof

per cases ;

suppose A29: i = 1 ; :: thesis:

len D in Seg (len D) by FINSEQ_1:5;
then 1 <= len D by FINSEQ_1:3;
then A30: 1 in Seg (len D) by FINSEQ_1:3;
then B30: 1 in dom D by FINSEQ_1:def 3;
then A31: ( lower_bound (divset D,1) = lower_bound A & upper_bound (divset D,1) = D . 1 ) by INTEGRA1:def 5;
(upper_bound (divset D1,j)) - (lower_bound A) >= (D . 1) - (lower_bound A) by A27, A29, XREAL_1:11;
then vol (divset D1,j) >= (upper_bound (divset D,1)) - (lower_bound (divset D,1)) by A28, A31, INTEGRA1:def 6;
then A32: vol (divset D1,j) >= vol (divset D,1) by INTEGRA1:def 6;
vol (divset D1,j) <= delta D1 by A25, Lm6;
then A33: delta D1 >= vol (divset D,1) by A32, XXREAL_0:2;
1 in Seg (len (upper_volume (chi A,A),D)) by A30, INTEGRA1:def 7;
then A34: 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 B30, INTEGRA1:22;
then vol (divset D,1) in rng (upper_volume (chi A,A),D) by A34, FUNCT_1:def 5;
then vol (divset D,1) >= min (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 7;
hence delta D1 >= min (rng (upper_volume (chi A,A),D)) by A33, XXREAL_0:2; :: thesis:

end;

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

then A36: ( lower_bound (divset D,i) = D . (i - 1) & upper_bound (divset D,i) = D . i ) by A24, INTEGRA1:def 5;
then A37: (upper_bound (divset D1,j)) - (lower_bound (divset D1,j)) >= (upper_bound (divset D,i)) - (lower_bound A) by A27, A28, XREAL_1:11;
D . (i - 1) in A by A24, A35, INTEGRA1:9;
then lower_bound A <= D . (i - 1) by INTEGRA2:1;
then (upper_bound (divset D,i)) - (lower_bound A) >= (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A36, XREAL_1:12;
then (upper_bound (divset D1,j)) - (lower_bound (divset D1,j)) >= (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by A37, XXREAL_0:2;
then vol (divset D1,j) >= (upper_bound (divset D,i)) - (lower_bound (divset D,i)) by INTEGRA1:def 6;
then A38: vol (divset D1,j) >= vol (divset D,i) by INTEGRA1:def 6;
vol (divset D1,j) <= delta D1 by A25, Lm6;
then A39: delta D1 >= vol (divset D,i) by A38, XXREAL_0:2;
A40: i in Seg (len D) by A24, FINSEQ_1:def 3;
then i in Seg (len (upper_volume (chi A,A),D)) by INTEGRA1:def 7;
then A41: i in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
i in dom D by A40, FINSEQ_1:def 3;
then vol (divset D,i) = (upper_volume (chi A,A),D) . i by INTEGRA1:22;
then vol (divset D,i) in rng (upper_volume (chi A,A),D) by A41, FUNCT_1:def 5;
then vol (divset D,i) >= min (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 7;
hence delta D1 >= min (rng (upper_volume (chi A,A),D)) by A39, XXREAL_0:2; :: thesis:

end;

hence contradiction by A19; :: thesis:

end;

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₁(D2, indx D2,D1,j) - H₁(D1,j) <= ($1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) );
A42: S₁[1]

proof

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

proof

A45: j <> 1 by A23, A43, A44;
then A46: ( j - 1 in NAT & j - 1 in dom D1 ) by A44, INTEGRA1:9;
reconsider j1 = j - 1 as Element of NAT by A44, A45, INTEGRA1:9;
( lower_bound (divset D1,j) <= D . 1 & D . 1 <= upper_bound (divset D1,j) ) by A44, INTEGRA2:1;
then A47: ( D1 . j1 <= D . 1 & D . 1 <= D1 . j ) by A44, A45, INTEGRA1:def 5;
A48: ( indx D2,D1,j1 in dom D2 & 1 <= indx D2,D1,j1 & indx D2,D1,j1 <= len D2 )

proof

thus indx D2,D1,j1 in dom D2 by A20, A46, INTEGRA1:def 21; :: thesis:
then indx D2,D1,j1 in Seg (len D2) by FINSEQ_1:def 3;
hence ( 1 <= indx D2,D1,j1 & indx D2,D1,j1 <= len D2 ) by FINSEQ_1:3; :: thesis:

end;

then mid D2,1,(indx D2,D1,j1) is increasing by INTEGRA1:37;
then A49: D2 | (indx D2,D1,j1) is increasing by A48, JORDAN3:25;
A50: ( j1 in dom D1 & 1 <= j1 & j1 <= len D1 )

proof

thus j1 in dom D1 by A44, A45, INTEGRA1:9; :: thesis:
j1 in Seg (len D1) by A46, FINSEQ_1:def 3;
hence ( 1 <= j1 & j1 <= len D1 ) by FINSEQ_1:3; :: thesis:

end;

then mid D1,1,j1 is increasing by INTEGRA1:37;
then A51: D1 | j1 is increasing by A50, JORDAN3:25;
A52: rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1)

proof

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
A53: ( k in dom (D2 | (indx D2,D1,j1)) & x1 = (D2 | (indx D2,D1,j1)) . k ) by PARTFUN1:26;
k in Seg (len (D2 | (indx D2,D1,j1))) by A53, FINSEQ_1:def 3;
then A54: k in Seg (indx D2,D1,j1) by A48, FINSEQ_1:80;
then A55: ( (D2 | (indx D2,D1,j1)) . k = D2 . k & k in dom D2 ) by A48, RFINSEQ:19;
then A56: D2 . k in rng D2 by FUNCT_1:def 5;
( 1 <= k & k <= indx D2,D1,j1 ) by A54, FINSEQ_1:3;
then D2 . k <= D2 . (indx D2,D1,j1) by A48, A55, GOBOARD2:18;
then A57: D2 . k <= D1 . j1 by A20, A46, INTEGRA1:def 21;
A58: len (D1 | j1) = j1 by A50, FINSEQ_1:80;
A59: ( 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
A60: ( n in dom D & D2 . k = D . n ) by PARTFUN1:26;
1 <= n by A60, FINSEQ_3:27;
then D . 1 <= D2 . k by A43, A60, GOBOARD2:18;
then D1 . j1 <= D2 . k by A47, XXREAL_0:2;
hence D2 . k = D1 . j1 by A57, XXREAL_0:1; :: thesis:

end;

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

proof

assume A62: D2 . k in rng D ; :: thesis:
j1 in Seg (len (D1 | j1)) by A50, A58, FINSEQ_1:3;
then j1 in dom (D1 | j1) by FINSEQ_1:def 3;
then A63: (D1 | j1) . j1 in rng (D1 | j1) by FUNCT_1:def 5;
j1 in Seg j1 by A50, FINSEQ_1:3;
hence D2 . k in rng (D1 | j1) by A50, A59, A62, A63, RFINSEQ:19; :: thesis:

end;

( 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
A64: ( m in dom D1 & D2 . k = D1 . m ) by PARTFUN1:26;
m in Seg (len D1) by A64, FINSEQ_1:def 3;
then A65: ( 1 <= m & m <= j1 ) by A50, A57, A64, FINSEQ_1:3, SEQM_3:def 1;
then A66: m in dom (D1 | j1) by A58, FINSEQ_3:27;
m in Seg j1 by A65, FINSEQ_1:3;
then D2 . k = (D1 | j1) . m by A50, A64, RFINSEQ:19;
hence D2 . k in rng (D1 | j1) by A66, FUNCT_1:def 5; :: thesis:

end;

hence x1 in rng (D1 | j1) by A20, A48, A53, A54, A56, A61, RFINSEQ:19, XBOOLE_0:def 3; :: thesis:

end;

then A67: rng (D2 | (indx D2,D1,j1)) c= rng (D1 | j1) by TARSKI:def 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
A68: ( k in dom (D1 | j1) & x1 = (D1 | j1) . k ) by PARTFUN1:26;
k in Seg (len (D1 | j1)) by A68, FINSEQ_1:def 3;
then A69: k in Seg j1 by A50, FINSEQ_1:80;
then A70: ( (D1 | j1) . k = D1 . k & k in dom D1 ) by A50, RFINSEQ:19;
then D1 . k in rng D1 by FUNCT_1:def 5;
then x1 in rng D2 by A20, A68, A70, XBOOLE_0:def 3;
then consider n being Element of NAT such that
A71: ( n in dom D2 & x1 = D2 . n ) by PARTFUN1:26;
A72: ( indx D2,D1,k in dom D2 & D2 . (indx D2,D1,k) = D2 . n ) by A20, A68, A70, A71, INTEGRA1:def 21;
k <= j1 by A69, FINSEQ_1:3;
then D1 . k <= D1 . j1 by A46, A70, GOBOARD2:18;
then D2 . (indx D2,D1,k) <= D1 . j1 by A20, A70, INTEGRA1:def 21;
then D2 . (indx D2,D1,k) <= D2 . (indx D2,D1,j1) by A20, A46, INTEGRA1:def 21;
then A73: n <= indx D2,D1,j1 by A48, A71, A72, SEQM_3:def 1;
1 <= n by A71, FINSEQ_3:27;
then A74: n in Seg (indx D2,D1,j1) by A73, FINSEQ_1:3;
then A75: D2 . n = (D2 | (indx D2,D1,j1)) . n by A48, RFINSEQ:19;
n in Seg (len (D2 | (indx D2,D1,j1))) by A48, A74, FINSEQ_1:80;
then n in dom (D2 | (indx D2,D1,j1)) by FINSEQ_1:def 3;
hence x1 in rng (D2 | (indx D2,D1,j1)) by A71, A75, FUNCT_1:def 5; :: thesis:

end;

then rng (D1 | j1) c= rng (D2 | (indx D2,D1,j1)) by TARSKI:def 3;
hence rng (D2 | (indx D2,D1,j1)) = rng (D1 | j1) by A67, XBOOLE_0:def 10; :: thesis:

end;

then A76: D2 | (indx D2,D1,j1) = D1 | j1 by A49, A51, Th5;
A77: 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 A78: ( 1 <= k & k <= j1 ) ; :: thesis:
assume A79: k <> indx D2,D1,k ; :: thesis:

now

per cases by A79, XXREAL_0:1;

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

( 1 <= k & k <= len D1 ) by A50, A78, XXREAL_0:2;
then A81: k in dom D1 by FINSEQ_3:27;
then A82: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A20, INTEGRA1:def 21;
then indx D2,D1,k in Seg (len D2) by FINSEQ_1:def 3;
then A83: ( 1 <= indx D2,D1,k & indx D2,D1,k <= indx D2,D1,j1 ) by A20, A50, A78, A81, Th6, FINSEQ_1:3;
then indx D2,D1,k in Seg (indx D2,D1,j1) by FINSEQ_1:3;
then A84: (D2 | (indx D2,D1,j1)) . (indx D2,D1,k) = D2 . (indx D2,D1,k) by A48, RFINSEQ:19;
A85: indx D2,D1,k < j1 by A78, A80, XXREAL_0:2;
then indx D2,D1,k <= len D1 by A50, XXREAL_0:2;
then indx D2,D1,k in dom D1 by A83, FINSEQ_3:27;
then A86: D1 . k > D1 . (indx D2,D1,k) by A80, A81, SEQM_3:def 1;
indx D2,D1,k in Seg j1 by A83, A85, FINSEQ_1:3;
hence contradiction by A50, A76, A82, A84, A86, RFINSEQ:19; :: thesis:

end;

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

k in Seg j1 by A78, FINSEQ_1:3;
then A88: D1 . k = (D1 | j1) . k by A46, RFINSEQ:19;
( 1 <= k & k <= len D1 ) by A50, A78, XXREAL_0:2;
then A89: k in dom D1 by FINSEQ_3:27;
then A90: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A20, INTEGRA1:def 21;
( indx D2,D1,k <= indx D2,D1,j1 & indx D2,D1,k in dom D2 & indx D2,D1,j1 in dom D2 ) by A20, A50, A78, A89, Th6;
then A91: k <= indx D2,D1,j1 by A87, XXREAL_0:2;
then k <= len D2 by A48, XXREAL_0:2;
then k in dom D2 by A78, FINSEQ_3:27;
then A92: D2 . k < D2 . (indx D2,D1,k) by A87, A90, SEQM_3:def 1;
k in Seg (indx D2,D1,j1) by A78, A91, FINSEQ_1:3;
hence contradiction by A48, A76, A88, A90, A92, RFINSEQ:19; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A93: len (D2 | (indx D2,D1,j1)) = len (D1 | j1) by A49, A51, A52, Th5;
len (D2 | (indx D2,D1,j1)) = indx D2,D1,j1 by A48, FINSEQ_1:80;
then A94: indx D2,D1,j1 = j1 by A50, A93, FINSEQ_1:80;
j1 <= len D1 by A46, FINSEQ_3:27;
then j1 <= len (lower_volume f,D1) by INTEGRA1:def 8;
then A95: len ((lower_volume f,D1) | j1) = indx D2,D1,j1 by A94, FINSEQ_1:80;
indx D2,D1,j1 in dom D2 by A20, A46, INTEGRA1:def 21;
then indx D2,D1,j1 <= len D2 by FINSEQ_3:27;
then indx D2,D1,j1 <= len (lower_volume f,D2) by INTEGRA1:def 8;
then A96: len ((lower_volume f,D1) | j1) = len ((lower_volume f,D2) | (indx D2,D1,j1)) by A95, FINSEQ_1:80;
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

let k be Nat; :: thesis:
assume A97: ( 1 <= k & k <= len ((lower_volume f,D1) | j1) ) ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A98: len (lower_volume f,D1) = len D1 by INTEGRA1:def 8;
then A99: ( 1 <= k & k <= j1 ) by A50, A97, FINSEQ_1:80;
then A100: k in Seg j1 by FINSEQ_1:3;
( 1 <= k & k <= len D1 ) by A50, A99, XXREAL_0:2;
then A101: k in Seg (len D1) by FINSEQ_1:3;
then B101: k in dom D1 by FINSEQ_1:def 3;
A102: divset D1,k = divset D2,(indx D2,D1,k)

proof

A103: divset D2,(indx D2,D1,k) = [.(lower_bound (divset D2,(indx D2,D1,k))),(upper_bound (divset D2,(indx D2,D1,k))).] by INTEGRA1:5;
A104: k in dom D1 by A101, FINSEQ_1:def 3;
then A105: ( indx D2,D1,k in dom D2 & D1 . k = D2 . (indx D2,D1,k) ) by A20, INTEGRA1:def 21;
( lower_bound (divset D1,k) = lower_bound (divset D2,(indx D2,D1,k)) & upper_bound (divset D1,k) = upper_bound (divset D2,(indx D2,D1,k)) )

proof

per cases ;

suppose A106: k = 1 ; :: thesis:

then A107: ( lower_bound (divset D1,k) = lower_bound A & upper_bound (divset D1,k) = D1 . k ) by A104, INTEGRA1:def 5;
indx D2,D1,k = 1 by A50, A77, A106;
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 A105, A107, INTEGRA1:def 5; :: thesis:

end;

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

then A109: ( lower_bound (divset D1,k) = D1 . (k - 1) & upper_bound (divset D1,k) = D1 . k ) by A104, INTEGRA1:def 5;
A110: ( k - 1 in dom D1 & D1 . (k - 1) in A & k - 1 in NAT ) by A104, A108, INTEGRA1:9;
reconsider k1 = k - 1 as Element of NAT by A104, A108, INTEGRA1:9;
k <= k + 1 by NAT_1:11;
then k1 <= k by XREAL_1:22;
then A111: k1 <= j1 by A99, XXREAL_0:2;
k1 in Seg (len D1) by A110, FINSEQ_1:def 3;
then 1 <= k1 by FINSEQ_1:3;
then A112: k1 = indx D2,D1,k1 by A77, A111;
indx D2,D1,k <> 1 by A77, A99, A108;
then A113: ( lower_bound (divset D2,(indx D2,D1,k)) = D2 . ((indx D2,D1,k) - 1) & upper_bound (divset D2,(indx D2,D1,k)) = D2 . (indx D2,D1,k) ) by A105, INTEGRA1:def 5;
D2 . ((indx D2,D1,k) - 1) = D2 . (indx D2,D1,k1) by A77, A99, A112;
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 A20, A104, A109, A110, A113, INTEGRA1:def 21; :: thesis:

end;

hence divset D1,k = divset D2,(indx D2,D1,k) by A103, INTEGRA1:5; :: thesis:

end;

j1 in Seg (len (lower_volume f,D1)) by A50, A98, FINSEQ_1:def 3;
then j1 in dom (lower_volume f,D1) by FINSEQ_1:def 3;
then A114: ((lower_volume f,D1) | j1) . k = (lower_volume f,D1) . k by A100, RFINSEQ:19
.= (lower_bound (rng (f | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by A102, B101, INTEGRA1:def 8 ;
indx D2,D1,k in Seg j1 by A77, A99, A100;
then A115: indx D2,D1,k in Seg (indx D2,D1,j1) by A50, A77;
then ( 1 <= indx D2,D1,k & indx D2,D1,k <= indx D2,D1,j1 ) by FINSEQ_1:3;
then ( 1 <= indx D2,D1,k & indx D2,D1,k <= len D2 ) by A48, XXREAL_0:2;
then indx D2,D1,k in Seg (len D2) by FINSEQ_1:3;
then B116: indx D2,D1,k in dom D2 by FINSEQ_1:def 3;
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 8;
then A117: indx D2,D1,j1 in dom (lower_volume f,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 A77, A99
.= (lower_volume f,D2) . (indx D2,D1,k) by A115, A117, RFINSEQ:19
.= (lower_bound (rng (f | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by B116, INTEGRA1:def 8 ;
hence ((lower_volume f,D1) | j1) . k = ((lower_volume f,D2) | (indx D2,D1,j1)) . k by A114; :: thesis:

end;

then A118: (lower_volume f,D2) | (indx D2,D1,j1) = (lower_volume f,D1) | j1 by A96, FINSEQ_1:18;
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 8;
then B119: indx D2,D1,j1 in dom (lower_volume f,D2) by FINSEQ_1:def 3;
j1 in Seg (len D1) by A50, FINSEQ_1:def 3;
then j1 in Seg (len (lower_volume f,D1)) by INTEGRA1:def 8;
then B120: j1 in dom (lower_volume f,D1) by FINSEQ_1:def 3;
A121: H₁(D2, indx D2,D1,j1) = Sum ((lower_volume f,D2) | (indx D2,D1,j1)) by B119, INTEGRA1:def 22
.= H₁(D1,j1) by A118, B120, INTEGRA1:def 22 ;
A122: (indx D2,D1,j1) + 1 <= indx D2,D1,j

proof

j < j + 1 by NAT_1:13;
then j1 < j by XREAL_1:21;
then indx D2,D1,j1 < indx D2,D1,j by A20, A44, A50, Th7;
hence (indx D2,D1,j1) + 1 <= indx D2,D1,j by NAT_1:13; :: thesis:

end;

A123: (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

A124: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len (lower_volume f,D2) )

proof

indx D2,D1,j in dom D2 by A20, A44, INTEGRA1:def 21;
then indx D2,D1,j in Seg (len D2) by FINSEQ_1:def 3;
then indx D2,D1,j in Seg (len (lower_volume f,D2)) by INTEGRA1:def 8;
hence ( 1 <= indx D2,D1,j & indx D2,D1,j <= len (lower_volume f,D2) ) by FINSEQ_1:3; :: thesis:

end;

then A125: ( 1 <= (indx D2,D1,j1) + 1 & (indx D2,D1,j1) + 1 <= len (lower_volume f,D2) ) by A48, A122, NAT_1:13, XXREAL_0:2;
A126: (indx D2,D1,j) - (indx D2,D1,j1) <= 2

proof

assume A127: (indx D2,D1,j) - (indx D2,D1,j1) > 2 ; :: thesis:
reconsider ID1 = (indx D2,D1,j1) + 1 as Element of NAT ;
reconsider ID2 = ID1 + 1 as Element of NAT ;
A128: ( indx D2,D1,j1 < ID1 & ID1 < ID2 & ID2 < indx D2,D1,j )

proof

thus indx D2,D1,j1 < ID1 by NAT_1:13; :: thesis:
thus ID1 < ID2 by NAT_1:13; :: thesis:
(indx D2,D1,j1) + (1 + 1) < indx D2,D1,j by A127, XREAL_1:22;
hence ID2 < indx D2,D1,j ; :: thesis:

end;

A129: indx D2,D1,j in dom D2 by A20, A44, INTEGRA1:def 21;
then A130: indx D2,D1,j <= len D2 by FINSEQ_3:27;
A131: ID1 in dom D2

proof

( 1 <= ID1 & ID1 <= indx D2,D1,j ) by A48, A128, XXREAL_0:2;
then ( 1 <= ID1 & ID1 <= len D2 ) by A130, XXREAL_0:2;
then ID1 in Seg (len D2) by FINSEQ_1:3;
hence ID1 in dom D2 by FINSEQ_1:def 3; :: thesis:

end;

A132: ID2 in dom D2

proof

( indx D2,D1,j1 <= ID2 & ID2 <= len D2 ) by A128, A130, XXREAL_0:2;
then ( 1 <= ID2 & ID2 <= len D2 ) by A48, XXREAL_0:2;
then ID2 in Seg (len D2) by FINSEQ_1:3;
hence ID2 in dom D2 by FINSEQ_1:def 3; :: thesis:

end;

then A133: ( D2 . (indx D2,D1,j1) < D2 . ID1 & D2 . ID1 < D2 . ID2 & D2 . ID2 < D2 . (indx D2,D1,j) ) by A48, A128, A129, A131, SEQM_3:def 1;
A134: ( D2 . ID1 in rng D & D2 . ID2 in rng D )

proof

A135: ( D2 . ID1 in (rng D) \/ (rng D1) & D2 . ID2 in (rng D) \/ (rng D1) ) by A20, A131, A132, FUNCT_1:def 5;
A136: ( D1 . j1 = D2 . (indx D2,D1,j1) & D1 . j = D2 . (indx D2,D1,j) ) by A20, A44, A50, INTEGRA1:def 21;
( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

proof

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

per cases by A137;

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

then consider n being Element of NAT such that
A138: ( n in dom D1 & D1 . n = D2 . ID1 ) by PARTFUN1:26;
( D2 . (indx D2,D1,j1) < D2 . ID1 & D2 . ID1 < D2 . (indx D2,D1,j) ) by A133, XXREAL_0:2;
then ( j1 < n & n < j ) by A44, A50, A136, A138, GOBOARD2:18;
then ( j < n + 1 & n < j ) by XREAL_1:21;
hence contradiction by NAT_1:13; :: thesis:

end;

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

then consider n being Element of NAT such that
A139: ( n in dom D1 & D1 . n = D2 . ID2 ) by PARTFUN1:26;
( D2 . (indx D2,D1,j1) < D2 . ID2 & D2 . ID2 < D2 . (indx D2,D1,j) ) by A133, XXREAL_0:2;
then ( j1 < n & n < j ) by A44, A50, A136, A139, GOBOARD2:18;
then ( j < n + 1 & n < j ) by XREAL_1:21;
hence contradiction by NAT_1:13; :: thesis:

end;

hence ( D2 . ID1 in rng D & D2 . ID2 in rng D ) by A135, XBOOLE_0:def 3; :: thesis:

end;

A140: ( lower_bound (divset D1,j) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,j) = D2 . (indx D2,D1,j) )

proof

( lower_bound (divset D1,j) = D1 . j1 & upper_bound (divset D1,j) = D1 . j ) by A44, A45, INTEGRA1:def 5;
hence ( lower_bound (divset D1,j) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,j) = D2 . (indx D2,D1,j) ) by A20, A44, A50, INTEGRA1:def 21; :: thesis:

end;

A141: D2 . ID1 in (rng D) /\ (divset D1,j)

proof

( D2 . (indx D2,D1,j1) <= D2 . ID1 & D2 . ID1 <= D2 . (indx D2,D1,j) ) by A133, XXREAL_0:2;
then D2 . ID1 in divset D1,j by A140, INTEGRA2:1;
hence D2 . ID1 in (rng D) /\ (divset D1,j) by A134, XBOOLE_0:def 4; :: thesis:

end;

D2 . ID2 in (rng D) /\ (divset D1,j)

proof

( D2 . (indx D2,D1,j1) <= D2 . ID2 & D2 . ID2 <= D2 . (indx D2,D1,j) ) by A133, XXREAL_0:2;
then D2 . ID2 in divset D1,j by A140, INTEGRA2:1;
hence D2 . ID2 in (rng D) /\ (divset D1,j) by A134, XBOOLE_0:def 4; :: thesis:

end;

hence contradiction by A19, A44, A128, A131, A132, A141, Th4, GOBOARD2:19; :: thesis:

end;

( 1 <= ((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 & ((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 <= 2 )

proof

A142: (indx D2,D1,j) -' ((indx D2,D1,j1) + 1) = (indx D2,D1,j) - ((indx D2,D1,j1) + 1) by A122, XREAL_1:235;
((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 >= 0 + 1 by XREAL_1:8;
hence ((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 >= 1 ; :: thesis:
thus ((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 <= 2 by A126, A142; :: thesis:

end;

then A143: ( 1 <= len (mid (lower_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) & len (mid (lower_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) <= 2 ) by A122, A124, A125, JORDAN3:27;
A144: ( 1 <= j & j <= len (lower_volume f,D1) )

proof

( 1 <= j & j <= len D1 ) by A44, FINSEQ_3:27;
hence ( 1 <= j & j <= len (lower_volume f,D1) ) by INTEGRA1:def 8; :: thesis:

end;

(j -' j) + 1 = 1 by Lm2;
then A145: len (mid (lower_volume f,D1),j,j) = 1 by A144, JORDAN3:27;
(mid (lower_volume f,D1),j,j) . 1 = (lower_volume f,D1) . j by A144, JORDAN3:27;
then mid (lower_volume f,D1),j,j = <*((lower_volume f,D1) . j)*> by A145, FINSEQ_1:57;
then A146: Sum (mid (lower_volume f,D1),j,j) = (lower_volume f,D1) . j by FINSOP_1:12;
A147: (indx D2,D1,j1) + 1 in Seg (len D2)

proof

(indx D2,D1,j1) + 1 in Seg (len (lower_volume f,D2)) by A125, FINSEQ_1:3;
hence (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 8; :: thesis:

end;

then B147: (indx D2,D1,j1) + 1 in dom D2 by FINSEQ_1:def 3;
j in Seg (len D1) by A44, FINSEQ_1:def 3;
then B148: j in dom D1 by FINSEQ_1:def 3;

now

per cases by A143, Lm3;

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

A150: (indx D2,D1,j1) + 1 = indx D2,D1,j

proof

((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 = 1 by A122, A124, A125, A149, JORDAN3:27;
then (indx D2,D1,j) - ((indx D2,D1,j1) + 1) = 0 by A122, XREAL_1:235;
hence (indx D2,D1,j1) + 1 = indx D2,D1,j ; :: thesis:

end;

A151: divset D2,(indx D2,D1,j) = divset D1,j

proof

( lower_bound (divset D1,j) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,j) = D2 . (indx D2,D1,j) )

proof

end;

then A152: divset D1,j = [.(D2 . (indx D2,D1,j1)),(D2 . (indx D2,D1,j)).] by INTEGRA1:5;
A153: (indx D2,D1,j) - 1 = indx D2,D1,j1 by A150;
A154: indx D2,D1,j in dom D2 by A20, A44, INTEGRA1:def 21;
indx D2,D1,j <> 1 by A48, A150, NAT_1:13;
then ( lower_bound (divset D2,(indx D2,D1,j)) = D2 . (indx D2,D1,j1) & upper_bound (divset D2,(indx D2,D1,j)) = D2 . (indx D2,D1,j) ) by A153, A154, INTEGRA1:def 5;
hence divset D2,(indx D2,D1,j) = divset D1,j by A152, INTEGRA1:5; :: thesis:

end;

(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 A124, A125, JORDAN3:27;
then mid (lower_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j) = <*((lower_volume f,D2) . ((indx D2,D1,j1) + 1))*> by A149, FINSEQ_1:57;
then A155: 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:12
.= (lower_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by B147, INTEGRA1:def 8
.= Sum (mid (lower_volume f,D1),j,j) by A146, A150, A151, B148, INTEGRA1:def 8 ;
A156: delta D1 >= 0 by Th8;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm4, XREAL_1:50;
then ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) >= 0 * (delta D1) by A156;
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 A155; :: thesis:

end;

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

A158: (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 A124, A125, JORDAN3:27;
(mid (lower_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 2 = (lower_volume f,D2) . ((indx D2,D1,j1) + 2)

proof

A159: 2 + ((indx D2,D1,j1) + 1) >= 0 + 1 by XREAL_1:9;
(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 A122, A124, A125, A157, JORDAN3:27
.= H₂(D2) . ((2 + ((indx D2,D1,j1) + 1)) - 1) by A159, XREAL_1:235
.= H₂(D2) . ((indx D2,D1,j1) + (1 + 1)) ;
hence (mid (lower_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 2 = (lower_volume f,D2) . ((indx D2,D1,j1) + 2) ; :: thesis:

end;

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 A157, A158, FINSEQ_1:61;
then A160: 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:107;
A161: vol (divset D1,j) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))

proof

A162: ( lower_bound (divset D1,j) = D2 . (indx D2,D1,j1) & upper_bound (divset D1,j) = D2 . (indx D2,D1,j) )

proof

end;

A163: indx D2,D1,j = (indx D2,D1,j1) + 2

proof

((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 = 2 by A122, A124, A125, A157, JORDAN3:27;
then ((indx D2,D1,j) - ((indx D2,D1,j1) + 1)) + 1 = 2 by A122, XREAL_1:235;
hence indx D2,D1,j = (indx D2,D1,j1) + 2 ; :: thesis:

end;

A164: ( lower_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 1) & upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2) & lower_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . ((indx D2,D1,j1) + 1) )

proof

A165: (indx D2,D1,j1) + 2 in dom D2 by A20, A44, A163, INTEGRA1:def 21;
(indx D2,D1,j1) + 1 in Seg (len (lower_volume f,D2)) by A125, FINSEQ_1:3;
then (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 8;
then A166: (indx D2,D1,j1) + 1 in dom D2 by FINSEQ_1:def 3;
A167: (indx D2,D1,j1) + 1 <> 1 by A48, NAT_1:13;
A168: ((indx D2,D1,j1) + 1) + 1 > 1 by A125, NAT_1:13;
A169: ((indx D2,D1,j1) + 2) - 1 = (indx D2,D1,j1) + 1 ;
A170: ((indx D2,D1,j1) + 1) - 1 = (indx D2,D1,j1) + 0 ;
thus ( lower_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 1) & upper_bound (divset D2,((indx D2,D1,j1) + 2)) = D2 . ((indx D2,D1,j1) + 2) ) by A165, A168, A169, INTEGRA1:def 5; :: thesis:
thus ( lower_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . (indx D2,D1,j1) & upper_bound (divset D2,((indx D2,D1,j1) + 1)) = D2 . ((indx D2,D1,j1) + 1) ) by A166, A167, A170, INTEGRA1:def 5; :: thesis:

end;

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 A162, A163, INTEGRA1:def 6;
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 A164, 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 A164 ;
hence vol (divset D1,j) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2))) by INTEGRA1:def 6; :: thesis:

end;

then A171: (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 B148, INTEGRA1:def 8;
A172: vol (divset D2,((indx D2,D1,j1) + 1)) >= 0 by INTEGRA1:11;
A173: vol (divset D2,((indx D2,D1,j1) + 2)) >= 0 by INTEGRA1:11;
A174: (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

A175: indx D2,D1,j in dom D2 by A20, A44, INTEGRA1:def 21;
A176: indx D2,D1,j = (indx D2,D1,j1) + 2

proof

end;

then (indx D2,D1,j1) + 2 in Seg (len D2) by A175, FINSEQ_1:def 3;
then B177: (indx D2,D1,j1) + 2 in dom D2 by FINSEQ_1:def 3;
set ID1 = (indx D2,D1,j1) + 1;
set ID2 = (indx D2,D1,j1) + 2;
A178: 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 A160, B177, INTEGRA1:def 8
.= ((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 B147, INTEGRA1:def 8 ;
divset D2,((indx D2,D1,j1) + 2) c= A by A175, A176, INTEGRA1:10;
then A179: lower_bound (rng (f | (divset D2,((indx D2,D1,j1) + 2)))) <= upper_bound (rng f) by A1, Lm5;
(indx D2,D1,j1) + 1 in dom D2 by A147, FINSEQ_1:def 3;
then divset D2,((indx D2,D1,j1) + 1) c= A by INTEGRA1:10;
then lower_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1)))) <= upper_bound (rng f) by A1, Lm5;
then A180: (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 A172, XREAL_1:66;
divset D1,j c= A by A44, INTEGRA1:10;
then lower_bound (rng (f | (divset D1,j))) >= lower_bound (rng f) by A1, Lm5;
then A181: ( (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))) & (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 A172, A173, XREAL_1:66;
(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 A173, A178, A179, XREAL_1:66;
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:22;
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:22;
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 A180, XXREAL_0:2;
then A182: 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:22;
reconsider A = lower_bound (rng (f | (divset D1,j))) as real number ;
set B = vol (divset D2,((indx D2,D1,j1) + 1));
set C = vol (divset D2,((indx D2,D1,j1) + 2));
((lower_volume f,D1) . j) - (A * (vol (divset D2,((indx D2,D1,j1) + 1)))) = A * (vol (divset D2,((indx D2,D1,j1) + 2))) by A171;
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 A146, A181, XREAL_1:21;
then (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:21;
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 A181, XXREAL_0:2;
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 XREAL_1:21;
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 A182, XREAL_1:15;
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, Lm4, 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 A44, Lm6, XREAL_1:66;
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 A161, A174, 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;

A183: 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)

proof

indx D2,D1,j in dom D2 by A20, A44, INTEGRA1:def 21;
then A184: indx D2,D1,j in Seg (len D2) by FINSEQ_1:def 3;
then A185: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len D2 ) by FINSEQ_1:3;
then A186: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len H₂(D2) ) by INTEGRA1:def 8;
indx D2,D1,j in Seg (len H₂(D2)) by A184, INTEGRA1:def 8;
then B187: indx D2,D1,j in dom H₂(D2) by FINSEQ_1:def 3;
A188: indx D2,D1,j1 < indx D2,D1,j by A122, NAT_1:13;
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 8;
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 (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:105
.= Sum ((mid H₂(D2),1,(indx D2,D1,j1)) ^ (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) by A48, JORDAN3:25
.= Sum (mid H₂(D2),1,(indx D2,D1,j)) by A48, A186, A188, INTEGRA2:4
.= Sum (H₂(D2) | (indx D2,D1,j)) by A185, JORDAN3:25 ;
hence 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 B187, INTEGRA1:def 22; :: thesis:

end;

H₁(D1,j1) + (Sum (mid (lower_volume f,D1),j,j)) = H₁(D1,j)

proof

A189: j in Seg (len D1) by A44, FINSEQ_1:def 3;
then A190: ( 1 <= j & j <= len D1 ) by FINSEQ_1:3;
then A191: ( 1 <= j & j <= len H₂(D1) ) by INTEGRA1:def 8;
j in Seg (len H₂(D1)) by A189, INTEGRA1:def 8;
then B192: j in dom H₂(D1) by FINSEQ_1:def 3;
j < j + 1 by NAT_1:13;
then A193: j1 < j by XREAL_1:21;
j1 in Seg (len D1) by A50, FINSEQ_1:def 3;
then j1 in Seg (len H₂(D1)) by INTEGRA1:def 8;
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 A50, JORDAN3:25
.= Sum (mid H₂(D1),1,j) by A50, A191, A193, INTEGRA2:4
.= Sum (H₂(D1) | j) by A190, JORDAN3:25 ;
hence H₁(D1,j1) + (Sum (mid (lower_volume f,D1),j,j)) = H₁(D1,j) by B192, INTEGRA1:def 22; :: thesis:

end;

hence H₁(D2, indx D2,D1,j) - H₁(D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A121, A123, A183; :: thesis:

end;

hence S₁[1] by A44; :: thesis:

end;

A194: for i being non empty Nat st S₁[i] holds
S₁[i + 1]

proof

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

proof

assume A197: i + 1 in dom D ; :: thesis:
then D . (i + 1) in A by INTEGRA1:8;
then consider j being Element of NAT such that
A198: ( j in dom D1 & D . (i + 1) in divset D1,j ) by Th2;
A199: ( 1 <= i + 1 & i + 1 <= len D ) by A197, FINSEQ_3:27;
i <= i + 1 by NAT_1:11;
then i <= len D by A199, XXREAL_0:2;
then A200: i in Seg (len D) by A196, FINSEQ_1:3;
then A201: i in dom D by FINSEQ_1:def 3;
consider n1 being Element of NAT such that
A202: ( n1 in dom D1 & D . i in divset D1,n1 & H₁(D2, indx D2,D1,n1) - H₁(D1,n1) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A195, A200, FINSEQ_1:def 3;
A203: ( indx D2,D1,n1 in dom D2 & D2 . (indx D2,D1,n1) = D1 . n1 ) by A20, A202, INTEGRA1:def 21;
then A204: ( 1 <= indx D2,D1,n1 & indx D2,D1,n1 <= len D2 ) by FINSEQ_3:27;
A205: n1 < j

proof

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

now

per cases by A206, XXREAL_0:1;

suppose n1 = j ; :: thesis:

then ( D . i in divset D1,j & D . i in rng D ) by A201, A202, FUNCT_1:def 5;
then A207: D . i in (rng D) /\ (divset D1,j) by XBOOLE_0:def 4;
D . (i + 1) in rng D by A197, FUNCT_1:def 5;
then A208: D . (i + 1) in (rng D) /\ (divset D1,j) by A198, XBOOLE_0:def 4;
i + 1 > i by XREAL_1:31;
hence contradiction by A19, A197, A198, A201, A207, A208, Th4, GOBOARD2:19; :: thesis:

end;

suppose n1 > j ; :: thesis:

then A209: n1 >= j + 1 by NAT_1:13;
then A210: n1 - 1 >= j by XREAL_1:21;
A211: lower_bound (divset D1,n1) <= D . i by A202, INTEGRA2:1;
A212: D . (i + 1) <= upper_bound (divset D1,j) by A198, INTEGRA2:1;
1 <= j by A198, FINSEQ_3:27;
then 1 + 1 <= j + 1 by XREAL_1:8;
then A213: n1 <> 1 by A209, XXREAL_0:2;
then n1 - 1 in dom D1 by A202, INTEGRA1:9;
then A214: D1 . j <= D1 . (n1 - 1) by A198, A210, GOBOARD2:18;
A215: upper_bound (divset D1,j) = D1 . j

proof

per cases ;

suppose j = 1 ; :: thesis:

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

end;

suppose j <> 1 ; :: thesis:

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

end;

D . i >= D1 . (n1 - 1) by A202, A211, A213, INTEGRA1:def 5;
then D . i >= D1 . j by A214, XXREAL_0:2;
then A216: D . i >= D . (i + 1) by A212, A215, XXREAL_0:2;
i < i + 1 by XREAL_1:31;
hence contradiction by A197, A201, A216, SEQM_3:def 1; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A217: n1 + 1 <= j by NAT_1:13;
then A218: j - n1 >= 1 by XREAL_1:21;
A219: n1 >= 1 by A202, FINSEQ_3:27;
A220: ( 1 <= n1 & 1 <= j & j <= len D1 ) by A198, A202, FINSEQ_3:27;
then A221: ( 1 <= n1 + 1 & n1 + 1 <= len D1 ) by A217, NAT_1:12, XXREAL_0:2;
then A222: n1 + 1 in dom D1 by FINSEQ_3:27;
then A223: ( indx D2,D1,(n1 + 1) in dom D2 & D2 . (indx D2,D1,(n1 + 1)) = D1 . (n1 + 1) ) by A20, INTEGRA1:def 21;
A224: ( indx D2,D1,j in dom D2 & D2 . (indx D2,D1,j) = D1 . j ) by A20, A198, INTEGRA1:def 21;
then D2 . (indx D2,D1,(n1 + 1)) <= D2 . (indx D2,D1,j) by A198, A217, A222, A223, GOBOARD2:18;
then A225: indx D2,D1,(n1 + 1) <= indx D2,D1,j by A223, A224, SEQM_3:def 1;
A226: ( 1 <= indx D2,D1,(n1 + 1) & indx D2,D1,(n1 + 1) <= len D2 ) by A223, FINSEQ_3:27;
A227: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len D2 ) by A224, FINSEQ_3:27;
n1 < n1 + 1 by NAT_1:13;
then D1 . n1 < D1 . (n1 + 1) by A202, A222, SEQM_3:def 1;
then A228: indx D2,D1,n1 < indx D2,D1,(n1 + 1) by A203, A223, GOBOARD2:18;
1 + (indx D2,D1,(n1 + 1)) <= (indx D2,D1,j) + 1 by A225, XREAL_1:8;
then 1 <= ((indx D2,D1,j) + 1) - (indx D2,D1,(n1 + 1)) by XREAL_1:21;
then A229: (mid D2,(indx D2,D1,(n1 + 1)),(indx D2,D1,j)) . 1 = D2 . ((1 - 1) + (indx D2,D1,(n1 + 1))) by A225, A226, A227, JORDAN3:31
.= D1 . (n1 + 1) by A20, A222, INTEGRA1:def 21 ;
A230: (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

per cases by A217, XXREAL_0:1;

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

A232: ( 1 <= n1 + 1 & n1 + 1 <= len H₂(D1) ) by A221, INTEGRA1:def 8;
n1 + 1 in Seg (len D1) by A222, FINSEQ_1:def 3;
then B233: n1 + 1 in dom D1 by FINSEQ_1:def 3;
A234: len (mid H₂(D1),(n1 + 1),j) = (j -' (n1 + 1)) + 1 by A231, A232, JORDAN3:27
.= (j - j) + 1 by A231, XREAL_1:235
.= 1 ;
(n1 + 1) + 1 <= j + 1 by A217, XREAL_1:8;
then 1 <= (j + 1) - (n1 + 1) by XREAL_1:21;
then (mid H₂(D1),(n1 + 1),j) . 1 = H₂(D1) . ((1 - 1) + (n1 + 1)) by A231, A232, JORDAN3:31
.= (lower_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))) by B233, INTEGRA1:def 8 ;
then mid H₂(D1),(n1 + 1),j = <*((lower_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))))*> by A234, FINSEQ_1:57;
then A235: Sum (mid H₂(D1),(n1 + 1),j) = (lower_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))) by FINSOP_1:12;
divset D1,(n1 + 1) c= A by A222, INTEGRA1:10;
then A236: lower_bound (rng (f | (divset D1,(n1 + 1)))) >= lower_bound (rng f) by A1, Lm5;
vol (divset D1,(n1 + 1)) >= 0 by INTEGRA1:11;
then A237: Sum (mid H₂(D1),(n1 + 1),j) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A235, A236, XREAL_1:66;
A238: indx D2,D1,n1 < indx D2,D1,j

proof

D1 . n1 < D1 . j by A198, A202, A205, SEQM_3:def 1;
hence indx D2,D1,n1 < indx D2,D1,j by A203, A224, GOBOARD2:18; :: thesis:

end;

then A239: (indx D2,D1,n1) + 1 <= indx D2,D1,j by NAT_1:13;
then (indx D2,D1,n1) + 1 <= len D2 by A227, XXREAL_0:2;
then A240: (indx D2,D1,n1) + 1 <= len H₂(D2) by INTEGRA1:def 8;
A241: 1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
A242: indx D2,D1,j <= len H₂(D2) by A227, INTEGRA1:def 8;
then A243: len (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) = ((indx D2,D1,j) -' ((indx D2,D1,n1) + 1)) + 1 by A227, A239, A240, A241, JORDAN3:27
.= ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A239, XREAL_1:235
.= (indx D2,D1,j) - (indx D2,D1,n1) ;
A244: (indx D2,D1,j) - (indx D2,D1,n1) <= 2

proof

assume (indx D2,D1,j) - (indx D2,D1,n1) > 2 ; :: thesis:
then A245: (indx D2,D1,n1) + 2 < indx D2,D1,j by XREAL_1:22;
A246: indx D2,D1,n1 < (indx D2,D1,n1) + 1 by NAT_1:13;
A247: (indx D2,D1,n1) + 1 < (indx D2,D1,n1) + 2 by XREAL_1:8;
A248: ( (indx D2,D1,n1) + 1 < indx D2,D1,j & (indx D2,D1,n1) + 1 in dom D2 )

proof

thus (indx D2,D1,n1) + 1 < indx D2,D1,j by A245, A247, XXREAL_0:2; :: thesis:
then ( 1 <= (indx D2,D1,n1) + 1 & (indx D2,D1,n1) + 1 <= len D2 ) by A204, A227, NAT_1:13, XXREAL_0:2;
hence (indx D2,D1,n1) + 1 in dom D2 by FINSEQ_3:27; :: thesis:

end;

A249: D2 . ((indx D2,D1,n1) + 1) in rng D

proof

A250: D2 . ((indx D2,D1,n1) + 1) in rng D2 by A248, FUNCT_1:def 5;
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
A251: ( k1 in dom D1 & D2 . ((indx D2,D1,n1) + 1) = D1 . k1 ) by PARTFUN1:26;
( D2 . (indx D2,D1,n1) < D2 . ((indx D2,D1,n1) + 1) & D2 . ((indx D2,D1,n1) + 1) < D2 . (indx D2,D1,j) ) by A203, A224, A246, A248, SEQM_3:def 1;
then ( n1 < k1 & k1 < j ) by A198, A202, A203, A224, A251, GOBOARD2:18;
hence contradiction by A231, NAT_1:13; :: thesis:

end;

hence D2 . ((indx D2,D1,n1) + 1) in rng D by A20, A250, XBOOLE_0:def 3; :: thesis:

end;

A252: D2 . ((indx D2,D1,n1) + 1) in (rng D) /\ (divset D1,j)

proof

A253: ( lower_bound (divset D1,j) = D1 . (j - 1) & upper_bound (divset D1,j) = D1 . j ) by A198, A205, A219, INTEGRA1:def 5;
( D2 . ((indx D2,D1,n1) + 1) >= D2 . (indx D2,D1,n1) & D2 . (indx D2,D1,j) >= D2 . ((indx D2,D1,n1) + 1) ) by A203, A224, A246, A248, GOBOARD2:18;
then D2 . ((indx D2,D1,n1) + 1) in divset D1,j by A203, A224, A231, A253, INTEGRA2:1;
hence D2 . ((indx D2,D1,n1) + 1) in (rng D) /\ (divset D1,j) by A249, XBOOLE_0:def 4; :: thesis:

end;

A254: ( indx D2,D1,n1 < (indx D2,D1,n1) + 2 & (indx D2,D1,n1) + 2 in dom D2 )

proof

thus indx D2,D1,n1 < (indx D2,D1,n1) + 2 by A247, NAT_1:13; :: thesis:
then ( 1 <= (indx D2,D1,n1) + 2 & (indx D2,D1,n1) + 2 <= len D2 ) by A204, A227, A245, XXREAL_0:2;
hence (indx D2,D1,n1) + 2 in dom D2 by FINSEQ_3:27; :: thesis:

end;

A255: D2 . ((indx D2,D1,n1) + 2) in rng D

proof

A256: D2 . ((indx D2,D1,n1) + 2) in rng D2 by A254, FUNCT_1:def 5;
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
A257: ( k1 in dom D1 & D2 . ((indx D2,D1,n1) + 2) = D1 . k1 ) by PARTFUN1:26;
( D2 . (indx D2,D1,n1) < D2 . ((indx D2,D1,n1) + 2) & D2 . ((indx D2,D1,n1) + 2) < D2 . (indx D2,D1,j) ) by A203, A224, A245, A254, SEQM_3:def 1;
then ( n1 < k1 & k1 < j ) by A198, A202, A203, A224, A257, GOBOARD2:18;
hence contradiction by A231, NAT_1:13; :: thesis:

end;

hence D2 . ((indx D2,D1,n1) + 2) in rng D by A20, A256, XBOOLE_0:def 3; :: thesis:

end;

D2 . ((indx D2,D1,n1) + 2) in (rng D) /\ (divset D1,j)

proof

A258: ( lower_bound (divset D1,j) = D1 . (j - 1) & upper_bound (divset D1,j) = D1 . j ) by A198, A205, A219, INTEGRA1:def 5;
( D2 . ((indx D2,D1,n1) + 2) >= D2 . (indx D2,D1,n1) & D2 . (indx D2,D1,j) >= D2 . ((indx D2,D1,n1) + 2) ) by A203, A224, A245, A254, GOBOARD2:18;
then D2 . ((indx D2,D1,n1) + 2) in divset D1,j by A203, A224, A231, A258, INTEGRA2:1;
hence D2 . ((indx D2,D1,n1) + 2) in (rng D) /\ (divset D1,j) by A255, XBOOLE_0:def 4; :: thesis:

end;

then D2 . ((indx D2,D1,n1) + 1) = D2 . ((indx D2,D1,n1) + 2) by A19, A198, A252, Th4;
hence contradiction by A247, A248, A254, SEQM_3:def 1; :: thesis:

end;

A259: ( (indx D2,D1,j) - (indx D2,D1,n1) = 1 or (indx D2,D1,j) - (indx D2,D1,n1) = 2 )

proof

(indx D2,D1,n1) + 1 <= indx D2,D1,j by A238, NAT_1:13;
then A260: ( (indx D2,D1,n1) + 1 = indx D2,D1,j or (indx D2,D1,n1) + 1 < indx D2,D1,j ) by XXREAL_0:1;
( (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 A261: ((indx D2,D1,n1) + 1) + 1 <= indx D2,D1,j by NAT_1:13;
(indx D2,D1,n1) + 2 >= indx D2,D1,j by A244, XREAL_1:22;
hence (indx D2,D1,n1) + 2 = indx D2,D1,j by A261, XXREAL_0:1; :: thesis:

end;

hence ( (indx D2,D1,j) - (indx D2,D1,n1) = 1 or (indx D2,D1,j) - (indx D2,D1,n1) = 2 ) by A260; :: thesis:

end;

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 A259;

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

then 1 = ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 ;
then A263: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 1 = H₂(D2) . ((1 + ((indx D2,D1,n1) + 1)) - 1) by A241, A242, JORDAN3:31
.= H₂(D2) . ((indx D2,D1,n1) + 1) ;
(indx D2,D1,n1) + 1 in Seg (len D2) by A224, A262, FINSEQ_1:def 3;
then (indx D2,D1,n1) + 1 in dom D2 by FINSEQ_1:def 3;
then A264: 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 8;
A265: divset D2,((indx D2,D1,n1) + 1) = divset D1,(n1 + 1)

proof

A266: divset D1,(n1 + 1) = [.(lower_bound (divset D1,(n1 + 1))),(upper_bound (divset D1,(n1 + 1))).] by INTEGRA1:5;
(indx D2,D1,n1) + 1 > 1 by A204, NAT_1:13;
then ( lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . (((indx D2,D1,n1) + 1) - 1) & upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . ((indx D2,D1,n1) + 1) ) by A224, A262, INTEGRA1:def 5;
then A267: ( lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D1 . n1 & upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D1 . j ) by A20, A198, A202, A262, INTEGRA1:def 21;
( lower_bound (divset D1,(n1 + 1)) = D1 . ((n1 + 1) - 1) & upper_bound (divset D1,(n1 + 1)) = D1 . (n1 + 1) ) by A205, A219, A222, A231, INTEGRA1:def 5;
hence divset D2,((indx D2,D1,n1) + 1) = divset D1,(n1 + 1) by A231, A266, A267, INTEGRA1:5; :: thesis:

end;

vol (divset D2,((indx D2,D1,n1) + 1)) >= 0 by INTEGRA1:11;
then A268: H₂(D2) . ((indx D2,D1,n1) + 1) <= (upper_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A1, A224, A262, A264, A265, Th17, XREAL_1:66;
mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j) = <*(H₂(D2) . ((indx D2,D1,n1) + 1))*> by A243, A262, A263, FINSEQ_1:57;
hence Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) <= (upper_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A268, FINSOP_1:12; :: thesis:

end;

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

A270: ((indx D2,D1,n1) + 2) - 1 = (indx D2,D1,n1) + 1 ;
A271: ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 >= 1 by A269;
A272: ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 = 1 + 1 by A269;
A273: ( 1 <= (indx D2,D1,n1) + 1 & (indx D2,D1,n1) + 1 <= (indx D2,D1,n1) + 2 ) by NAT_1:12, XREAL_1:8;
then (indx D2,D1,n1) + 1 <= len D2 by A227, A269, XXREAL_0:2;
then A274: (indx D2,D1,n1) + 1 in dom D2 by A273, FINSEQ_3:27;
A275: indx D2,D1,j <= len H₂(D2) by A227, INTEGRA1:def 8;
then A276: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 1 = H₂(D2) . ((1 + ((indx D2,D1,n1) + 1)) - 1) by A269, A271, A273, JORDAN3:31
.= H₂(D2) . ((indx D2,D1,n1) + 1) ;
(mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 2 = H₂(D2) . ((2 + ((indx D2,D1,n1) + 1)) - 1) by A272, A273, A275, JORDAN3:31
.= H₂(D2) . (((indx D2,D1,n1) + 0 ) + 2) ;
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 A243, A269, A276, FINSEQ_1:61;
then A277: 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;
A278: H₂(D2) . ((indx D2,D1,n1) + 1) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1)))

proof

(indx D2,D1,n1) + 1 in Seg (len D2) by A274, FINSEQ_1:def 3;
then (indx D2,D1,n1) + 1 in dom D2 by FINSEQ_1:def 3;
then A279: 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 8;
vol (divset D2,((indx D2,D1,n1) + 1)) >= 0 by INTEGRA1:11;
hence H₂(D2) . ((indx D2,D1,n1) + 1) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1))) by A1, A274, A279, Th17, XREAL_1:66; :: thesis:

end;

H₂(D2) . ((indx D2,D1,n1) + 2) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 2)))

proof

(indx D2,D1,n1) + 2 in Seg (len D2) by A224, A269, FINSEQ_1:def 3;
then (indx D2,D1,n1) + 2 in dom D2 by FINSEQ_1:def 3;
then A280: 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 INTEGRA1:def 8;
vol (divset D2,((indx D2,D1,n1) + 2)) >= 0 by INTEGRA1:11;
hence H₂(D2) . ((indx D2,D1,n1) + 2) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 2))) by A1, A224, A269, A280, Th17, XREAL_1:66; :: thesis:

end;

then A281: 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 A277, A278, XREAL_1:9;
(vol (divset D2,((indx D2,D1,n1) + 1))) + (vol (divset D2,((indx D2,D1,n1) + 2))) = vol (divset D1,(n1 + 1))

proof

(indx D2,D1,n1) + 1 > 1 by A204, NAT_1:13;
then A282: ( lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . (((indx D2,D1,n1) + 1) - 1) & upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D2 . ((indx D2,D1,n1) + 1) ) by A274, INTEGRA1:def 5;
(indx D2,D1,n1) + 2 >= 2 + 1 by A204, XREAL_1:8;
then (indx D2,D1,n1) + 2 <> 1 ;
then A283: ( lower_bound (divset D2,((indx D2,D1,n1) + 2)) = D2 . ((indx D2,D1,n1) + 1) & upper_bound (divset D2,((indx D2,D1,n1) + 2)) = D2 . (indx D2,D1,j) ) by A224, A269, A270, INTEGRA1:def 5;
A284: vol (divset D2,((indx D2,D1,n1) + 1)) = (D2 . ((indx D2,D1,n1) + 1)) - (D1 . n1) by A203, A282, INTEGRA1:def 6;
A285: vol (divset D2,((indx D2,D1,n1) + 2)) = (D1 . j) - (D2 . ((indx D2,D1,n1) + 1)) by A224, A283, INTEGRA1:def 6;
( lower_bound (divset D1,(n1 + 1)) = D1 . ((n1 + 1) - 1) & upper_bound (divset D1,(n1 + 1)) = D1 . (n1 + 1) ) by A205, A219, A222, A231, INTEGRA1:def 5;
then vol (divset D1,(n1 + 1)) = (D1 . (n1 + 1)) - (D1 . n1) by INTEGRA1:def 6;
hence (vol (divset D2,((indx D2,D1,n1) + 1))) + (vol (divset D2,((indx D2,D1,n1) + 2))) = vol (divset D1,(n1 + 1)) by A231, A284, A285; :: thesis:

end;

hence Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) <= (upper_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A281; :: thesis:

end;

then A286: (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 A237, XREAL_1:15;
A287: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm4, XREAL_1:50;
vol (divset D1,(n1 + 1)) <= delta D1

proof

A288: n1 + 1 in Seg (len D1) by A222, FINSEQ_1:def 3;
then n1 + 1 in dom D1 by FINSEQ_1:def 3;
then A289: vol (divset D1,(n1 + 1)) = (upper_volume (chi A,A),D1) . (n1 + 1) by INTEGRA1:22;
n1 + 1 in Seg (len (upper_volume (chi A,A),D1)) by A288, INTEGRA1:def 7;
then n1 + 1 in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then A290: vol (divset D1,(n1 + 1)) in rng (upper_volume (chi A,A),D1) by A289, FUNCT_1:def 5;
delta D1 = max (rng (upper_volume (chi A,A),D1)) by INTEGRA1:def 19;
hence vol (divset D1,(n1 + 1)) <= delta D1 by A290, XXREAL_2:def 8; :: thesis:

end;

then ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset D1,(n1 + 1))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A287, XREAL_1:66;
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 A286, XXREAL_0:2; :: thesis:

end;

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

A292: n1 < n1 + 1 by NAT_1:13;
then A293: D1 . n1 < D1 . (n1 + 1) by A202, A222, SEQM_3:def 1;
then consider B being closed-interval Subset of REAL , MD1, MD2 being Division of B such that
A294: ( D1 . n1 = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid D1,(n1 + 1),j & MD2 = mid D2,(indx D2,D1,(n1 + 1)),(indx D2,D1,j) ) by A20, A198, A217, A222, A229, Th14;
A295: len MD1 = (j -' (n1 + 1)) + 1 by A217, A220, A221, A294, JORDAN3:27;
j -' (n1 + 1) = j - (n1 + 1) by A217, XREAL_1:235;
then A296: (j -' (n1 + 1)) + 1 = j - n1 ;
then A297: len MD1 = j - n1 by A217, A220, A221, A294, JORDAN3:27;
A298: ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A217, A295, XREAL_1:235
.= j ;
A299: B c= A

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis:
assume A300: x1 in B ; :: thesis:
then reconsider x1 = x1 as Real ;
A301: rng D1 c= A by INTEGRA1:def 2;
A302: ( D1 . n1 <= x1 & x1 <= MD1 . (len MD1) ) by A294, A300, INTEGRA2:1;
( D1 . n1 in rng D1 & D1 . j in rng D1 ) by A198, A202, FUNCT_1:def 5;
then A303: ( lower_bound A <= D1 . n1 & D1 . j <= upper_bound A ) by A301, INTEGRA2:1;
MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A217, A218, A220, A221, A294, A296, A297, JORDAN3:31
.= D1 . j ;
then ( lower_bound A <= x1 & x1 <= upper_bound A ) by A302, A303, XXREAL_0:2;
hence x1 in A by INTEGRA2:1; :: thesis:

end;

then reconsider g = f | B as Function of B,REAL by FUNCT_2:38;
A304: g | B is bounded

proof

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

proof

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

end;

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

proof

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

end;

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

end;

rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:34;
then A313: 1 <= len MD2 by FINSEQ_3:27;
A314: len MD2 = ((indx D2,D1,j) -' (indx D2,D1,(n1 + 1))) + 1 by A225, A226, A227, A294, JORDAN3:27;
then A315: len MD2 = ((indx D2,D1,j) - (indx D2,D1,(n1 + 1))) + 1 by A225, XREAL_1:235;
then A316: ((len MD2) - 1) + (indx D2,D1,(n1 + 1)) = indx D2,D1,j ;
A317: rng MD2 = (rng MD1) \/ {(D . (i + 1))}

proof

for x1 being set st x1 in rng MD2 holds
x1 in (rng MD1) \/ {(D . (i + 1))}

proof

let x1 be set ; :: thesis:
assume A318: x1 in rng MD2 ; :: thesis:
then reconsider x1 = x1 as Real ;
A319: MD2 . 1 = D2 . (indx D2,D1,(n1 + 1)) by A226, A227, A294, JORDAN3:27;
MD2 . (len MD2) = D2 . (indx D2,D1,j) by A225, A226, A227, A294, A313, A314, A316, JORDAN3:31;
then A320: ( D1 . (n1 + 1) <= x1 & x1 <= D1 . j ) by A223, A224, A318, A319, Th15;
A321: rng MD2 c= rng D2 by A294, JORDAN3:28;

now

per cases by A20, A318, A321, XBOOLE_0:def 3;

suppose x1 in rng D1 ; :: thesis:

then consider k being Element of NAT such that
A322: ( k in dom D1 & D1 . k = x1 ) by PARTFUN1:26;
A323: ( n1 + 1 <= k & k <= j ) by A198, A222, A320, A322, SEQM_3:def 1;
then A324: ( 1 <= k - n1 & k - n1 <= len MD1 ) by A297, XREAL_1:11, XREAL_1:21;
(j - (n1 + 1)) + 1 = j - n1 ;
then A325: k - n1 <= (j - (n1 + 1)) + 1 by A323, XREAL_1:11;
n1 <= n1 + 1 by NAT_1:11;
then n1 <= k by A323, XXREAL_0:2;
then consider n being Nat such that
A326: k = n1 + n by NAT_1:10;
n in dom MD1 by A324, A326, FINSEQ_3:27;
then A327: 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 A217, A220, A221, A294, A324, A325, A326, JORDAN3:31
.= D1 . k ;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by A322, A327, XBOOLE_0:def 3; :: thesis:

end;

suppose x1 in rng D ; :: thesis:

then consider n being Element of NAT such that
A328: ( n in dom D & D . n = x1 ) by PARTFUN1:26;
A329: D . i <= upper_bound (divset D1,n1) by A202, INTEGRA2:1;
upper_bound (divset D1,n1) = D1 . n1

proof

per cases ;

suppose n1 = 1 ; :: thesis:

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

end;

suppose n1 <> 1 ; :: thesis:

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

end;

then D . i < D1 . (n1 + 1) by A293, A329, XXREAL_0:2;
then D . i < D . n by A320, A328, XXREAL_0:2;
then i < n by A201, A328, GOBOARD2:18;
then i + 1 <= n by NAT_1:13;
then A330: ( i + 1 = n or i + 1 < n ) by XXREAL_0:1;
not i + 1 < n

proof

assume i + 1 < n ; :: thesis:
then A331: D . (i + 1) < D . n by A197, A328, SEQM_3:def 1;
lower_bound (divset D1,j) <= D . (i + 1) by A198, INTEGRA2:1;
then A332: lower_bound (divset D1,j) <= D . n by A331, XXREAL_0:2;
upper_bound (divset D1,j) = D1 . j

proof

per cases ;

suppose j = 1 ; :: thesis:

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

end;

suppose j <> 1 ; :: thesis:

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

end;

then ( D . n in rng D & D . n in divset D1,j ) by A320, A328, A332, FUNCT_1:def 5, INTEGRA2:1;
then A333: x1 in (rng D) /\ (divset D1,j) by A328, XBOOLE_0:def 4;
A334: D . (i + 1) in rng D by A197, FUNCT_1:def 5;
consider y1 being Real such that
A335: y1 = D . (i + 1) ;
y1 in (rng D) /\ (divset D1,j) by A198, A334, A335, XBOOLE_0:def 4;
hence contradiction by A19, A198, A328, A331, A333, A335, Th4; :: thesis:

end;

then x1 in {(D . (i + 1))} by A328, A330, 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 A336: rng MD2 c= (rng MD1) \/ {(D . (i + 1))} by TARSKI:def 3;
for x1 being set st x1 in (rng MD1) \/ {(D . (i + 1))} holds
x1 in rng MD2

proof

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

now

per cases by A337, XBOOLE_0:def 3;

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

rng MD1 c= rng D1 by A294, JORDAN3:28;
then A339: x1 in rng D1 by A338;
rng MD1 <> {} ;
then 1 in dom MD1 by FINSEQ_3:34;
then A340: 1 <= len MD1 by FINSEQ_3:27;
A341: len MD1 = (j -' (n1 + 1)) + 1 by A217, A220, A221, A294, JORDAN3:27;
A342: MD1 . 1 = D1 . (n1 + 1) by A220, A221, A294, JORDAN3:27;
((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A217, A341, XREAL_1:235
.= j ;
then MD1 . (len MD1) = D1 . j by A217, A220, A221, A294, A340, A341, JORDAN3:31;
then A343: ( D2 . (indx D2,D1,(n1 + 1)) <= x1 & x1 <= D2 . (indx D2,D1,j) ) by A223, A224, A338, A342, Th15;
rng D1 c= rng D2 by A20, INTEGRA1:def 20;
then consider k being Element of NAT such that
A344: ( k in dom D2 & D2 . k = x1 ) by A339, PARTFUN1:26;
A345: ( indx D2,D1,(n1 + 1) <= k & k <= indx D2,D1,j ) by A223, A224, A343, A344, SEQM_3:def 1;
then (indx D2,D1,(n1 + 1)) + 1 <= k + 1 by XREAL_1:8;
then A346: 1 <= (k + 1) - (indx D2,D1,(n1 + 1)) by XREAL_1:21;
k - (indx D2,D1,(n1 + 1)) <= (indx D2,D1,j) - (indx D2,D1,(n1 + 1)) by A345, XREAL_1:11;
then A347: (k - (indx D2,D1,(n1 + 1))) + 1 <= ((indx D2,D1,j) - (indx D2,D1,(n1 + 1))) + 1 by XREAL_1:8;
indx D2,D1,(n1 + 1) <= k + 1 by A345, NAT_1:12;
then consider n being Nat such that
A348: k + 1 = (indx D2,D1,(n1 + 1)) + n by NAT_1:10;
A349: n in dom MD2 by A315, A346, A347, A348, FINSEQ_3:27;
n in NAT by ORDINAL1:def 13;
then MD2 . n = D2 . ((n + (indx D2,D1,(n1 + 1))) - 1) by A225, A226, A227, A294, A346, A347, A348, JORDAN3:31
.= D2 . k by A348 ;
hence x1 in rng MD2 by A344, A349, FUNCT_1:def 5; :: thesis:

end;

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

then A350: x1 = D . (i + 1) by TARSKI:def 1;
A351: D . (i + 1) in rng D by A197, FUNCT_1:def 5;
rng D c= rng D2 by A20, INTEGRA1:def 20;
then consider k being Element of NAT such that
A352: ( k in dom D2 & x1 = D2 . k ) by A350, A351, PARTFUN1:26;
( lower_bound (divset D1,j) <= D . (i + 1) & D . (i + 1) <= upper_bound (divset D1,j) ) by A198, INTEGRA2:1;
then A353: ( D1 . (j - 1) <= x1 & x1 <= D1 . j ) by A198, A205, A219, A350, INTEGRA1:def 5;
A354: ( j - 1 in dom D1 & j - 1 in NAT ) by A198, A205, A219, INTEGRA1:9;
reconsider j1 = j - 1 as Element of NAT by A198, A205, A219, INTEGRA1:9;
n1 < j1 by A291, XREAL_1:22;
then n1 + 1 <= j1 by NAT_1:13;
then D1 . (n1 + 1) <= D1 . (j - 1) by A222, A354, GOBOARD2:18;
then ( D2 . (indx D2,D1,(n1 + 1)) <= D2 . k & D2 . k <= D2 . (indx D2,D1,j) ) by A20, A198, A223, A352, A353, INTEGRA1:def 21, XXREAL_0:2;
hence x1 in rng MD2 by A223, A224, A294, A352, Th16; :: thesis:

end;

hence x1 in rng MD2 ; :: thesis:

end;

then (rng MD1) \/ {(D . (i + 1))} c= rng MD2 by TARSKI:def 3;
hence rng MD2 = (rng MD1) \/ {(D . (i + 1))} by A336, XBOOLE_0:def 10; :: thesis:

end;

A355: len MD1 in dom MD1 by FINSEQ_5:6;
then A356: 1 <= len MD1 by FINSEQ_3:27;
A357: ( 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 A358: len MD1 = 1 ; :: thesis:

then A359: ( lower_bound (divset MD1,(len MD1)) = lower_bound B & upper_bound (divset MD1,(len MD1)) = MD1 . (len MD1) ) by A355, INTEGRA1:def 5;
( lower_bound (divset D1,j) = D1 . (j - 1) & upper_bound (divset D1,j) = D1 . j ) by A198, A205, A219, 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 A220, A294, A298, A358, A359, JORDAN3:27; :: thesis:

end;

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

then A361: ( lower_bound (divset MD1,(len MD1)) = MD1 . ((len MD1) - 1) & upper_bound (divset MD1,(len MD1)) = MD1 . (len MD1) ) by A355, INTEGRA1:def 5;
A362: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A297;
( (len MD1) - 1 in dom MD1 & (len MD1) - 1 in NAT ) by A355, A360, INTEGRA1:9;
then A363: (len MD1) - 1 >= 1 by Lm1;
len MD1 <= (len MD1) + 1 by NAT_1:11;
then (len MD1) - 1 <= len MD1 by XREAL_1:22;
then A364: lower_bound (divset MD1,(len MD1)) = D1 . (j - 1) by A217, A220, A221, A294, A295, A361, A362, A363, JORDAN3:31;
upper_bound (divset MD1,(len MD1)) = D1 . j by A217, A220, A221, A294, A295, A298, A356, A361, 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 A198, A205, A219, A364, INTEGRA1:def 5; :: thesis:

end;

( lower_bound (divset D1,j) <= D . (i + 1) & D . (i + 1) <= upper_bound (divset D1,j) ) by A198, INTEGRA2:1;
then A365: D . (i + 1) in divset MD1,(len MD1) by A357, INTEGRA2:1;
A366: (Sum (lower_volume g,MD2)) - (Sum (lower_volume g,MD1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1)

proof

( vol B <> 0 & D . (i + 1) > lower_bound B )

proof

A367: vol B = (upper_bound B) - (D1 . n1) by A294, INTEGRA1:def 6;
A368: len MD1 in dom MD1 by FINSEQ_5:6;
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 A368, INTEGRA1:def 5; :: thesis:

end;

suppose len MD1 <> 1 ; :: thesis:

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

end;

then vol B = (D1 . j) - (D1 . n1) by A198, A205, A219, A294, A357, A367, INTEGRA1:def 5;
hence vol B <> 0 by A198, A202, A205, SEQM_3:def 1; :: thesis:
lower_bound (divset D1,j) <= D . (i + 1) by A198, INTEGRA2:1;
then A369: D1 . (j - 1) <= D . (i + 1) by A198, A205, A219, INTEGRA1:def 5;
A370: n1 < j - 1 by A291, XREAL_1:22;
j - 1 in dom D1 by A198, A205, A219, INTEGRA1:9;
then D1 . n1 < D1 . (j - 1) by A202, A370, SEQM_3:def 1;
hence D . (i + 1) > lower_bound B by A294, A369, XXREAL_0:2; :: thesis:

end;

hence (Sum (lower_volume g,MD2)) - (Sum (lower_volume g,MD1)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A294, A304, A317, A365, Th12; :: thesis:

end;

A371: rng g c= rng f by RELAT_1:99;
( f | A is bounded_above & f | A is bounded_below ) by A1;
then ( rng f is bounded_above & rng f is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
then ( upper_bound (rng f) >= upper_bound (rng g) & lower_bound (rng f) <= lower_bound (rng g) ) by A371, SEQ_4:64, SEQ_4:65;
then A372: (upper_bound (rng f)) - (lower_bound (rng f)) >= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:15;
delta MD1 >= 0 by Th8;
then ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A372, XREAL_1:66;
then A373: (Sum (lower_volume g,MD2)) - (Sum (lower_volume g,MD1)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A366, XXREAL_0:2;
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
A374: ( k in dom (upper_volume (chi B,B),MD1) & (upper_volume (chi B,B),MD1) . k = delta MD1 ) by PARTFUN1:26;
k in Seg (len (upper_volume (chi B,B),MD1)) by A374, FINSEQ_1:def 3;
then A375: k in Seg (len MD1) by INTEGRA1:def 7;
then k in dom MD1 by FINSEQ_1:def 3;
then A376: delta MD1 = vol (divset MD1,k) by A374, INTEGRA1:22;
n1 + 1 > 1 by A219, NAT_1:13;
then n1 > 1 - 1 by XREAL_1:21;
then A377: ( 1 <= k & k <= len MD1 & k < k + n1 ) by A375, FINSEQ_1:3, XREAL_1:31;
then A378: 1 < k + n1 by XXREAL_0:2;
A379: k in dom MD1 by A375, FINSEQ_1:def 3;
k + n1 <= j by A297, A377, XREAL_1:21;
then k + n1 <= len D1 by A220, XXREAL_0:2;
then A380: k + n1 in dom D1 by A378, FINSEQ_3:27;
A381: divset MD1,k = divset D1,(k + n1)

proof

( 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 A382: k = 1 ; :: thesis:

then ( lower_bound (divset MD1,k) = lower_bound B & upper_bound (divset MD1,k) = MD1 . k ) by A379, INTEGRA1:def 5;
then A383: ( lower_bound (divset MD1,k) = D1 . n1 & upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) ) by A217, A220, A221, A294, A295, A377, JORDAN3:31;
( lower_bound (divset D1,(k + n1)) = D1 . ((k + n1) - 1) & upper_bound (divset D1,(k + n1)) = D1 . (k + n1) ) by A377, A380, 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 A382, A383; :: thesis:

end;

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

then A385: ( k - 1 in dom MD1 & k - 1 in NAT ) by A379, INTEGRA1:9;
then A386: ( 1 <= k - 1 & k - 1 <= len MD1 ) by Lm1;
( lower_bound (divset MD1,k) = MD1 . (k - 1) & upper_bound (divset MD1,k) = MD1 . k ) by A379, A384, INTEGRA1:def 5;
then ( lower_bound (divset MD1,k) = D1 . (((k - 1) + (n1 + 1)) - 1) & upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) ) by A217, A220, A221, A294, A295, A377, A385, A386, 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 A377, A380, INTEGRA1:def 5; :: thesis:

end;

then divset MD1,k = [.(lower_bound (divset D1,(k + n1))),(upper_bound (divset D1,(k + n1))).] by INTEGRA1:5;
hence divset MD1,k = divset D1,(k + n1) by INTEGRA1:5; :: thesis:

end;

A387: k + n1 in Seg (len D1) by A380, FINSEQ_1:def 3;
then k + n1 in dom D1 by FINSEQ_1:def 3;
then A388: delta MD1 = (upper_volume (chi A,A),D1) . (k + n1) by A376, A381, INTEGRA1:22;
k + n1 in Seg (len (upper_volume (chi A,A),D1)) by A387, INTEGRA1:def 7;
then k + n1 in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then delta MD1 in rng (upper_volume (chi A,A),D1) by A388, FUNCT_1:def 5;
then delta MD1 <= max (rng (upper_volume (chi A,A),D1)) by XXREAL_2:def 8;
then A389: delta MD1 <= delta D1 by INTEGRA1:def 19;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm4, XREAL_1:50;
then A390: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A389, XREAL_1:66;
A391: indx D2,D1,n1 < (indx D2,D1,n1) + 1 by NAT_1:13;
A392: 1 <= (indx D2,D1,n1) + 1 by A204, NAT_1:13;
D1 . n1 < D1 . (n1 + 1) by A202, A222, A292, SEQM_3:def 1;
then indx D2,D1,n1 < indx D2,D1,(n1 + 1) by A203, A223, GOBOARD2:18;
then A393: (indx D2,D1,n1) + 1 <= indx D2,D1,(n1 + 1) by NAT_1:13;
then A394: (indx D2,D1,n1) + 1 <= len D2 by A226, XXREAL_0:2;
then A395: (indx D2,D1,n1) + 1 <= len H₂(D2) by INTEGRA1:def 8;
A396: indx D2,D1,(n1 + 1) = (indx D2,D1,n1) + 1

proof

assume indx D2,D1,(n1 + 1) <> (indx D2,D1,n1) + 1 ; :: thesis:
then A397: indx D2,D1,(n1 + 1) > (indx D2,D1,n1) + 1 by A393, XXREAL_0:1;
A398: (indx D2,D1,n1) + 1 in dom D2 by A392, A394, FINSEQ_3:27;
then A399: D2 . ((indx D2,D1,n1) + 1) in rng D2 by FUNCT_1:def 5;

now

per cases by A20, A399, XBOOLE_0:def 3;

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

then consider n2 being Element of NAT such that
A400: ( n2 in dom D1 & D2 . ((indx D2,D1,n1) + 1) = D1 . n2 ) by PARTFUN1:26;
D2 . (indx D2,D1,n1) < D2 . ((indx D2,D1,n1) + 1) by A203, A391, A398, SEQM_3:def 1;
then n1 < n2 by A202, A203, A400, GOBOARD2:18;
then A401: n1 + 1 <= n2 by NAT_1:13;
D1 . n2 < D1 . (n1 + 1) by A223, A397, A398, A400, SEQM_3:def 1;
hence contradiction by A222, A400, A401, GOBOARD2:18; :: thesis:

end;

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

then consider n2 being Element of NAT such that
A402: ( n2 in dom D & D2 . ((indx D2,D1,n1) + 1) = D . n2 ) by PARTFUN1:26;
A403: D1 . n1 < D . n2 by A203, A391, A398, A402, SEQM_3:def 1;
A404: D . i <= upper_bound (divset D1,n1) by A202, INTEGRA2:1;
upper_bound (divset D1,n1) = D1 . n1

proof

per cases ;

suppose n1 = 1 ; :: thesis:

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

end;

suppose n1 <> 1 ; :: thesis:

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

end;

then D . i < D . n2 by A403, A404, XXREAL_0:2;
then i < n2 by A201, A402, GOBOARD2:18;
then A405: i + 1 <= n2 by NAT_1:13;
A406: D . n2 < D1 . (n1 + 1) by A223, A397, A398, A402, SEQM_3:def 1;
A407: ( j - 1 in dom D1 & j - 1 in NAT ) by A198, A205, A219, INTEGRA1:9;
(n1 + 1) + 1 <= j by A291, NAT_1:13;
then n1 + 1 <= j - 1 by XREAL_1:21;
then A408: D1 . (n1 + 1) <= D1 . (j - 1) by A222, A407, GOBOARD2:18;
A409: lower_bound (divset D1,j) <= D . (i + 1) by A198, INTEGRA2:1;
lower_bound (divset D1,j) = D1 . (j - 1) by A198, A205, A219, INTEGRA1:def 5;
then D1 . (n1 + 1) <= D . (i + 1) by A408, A409, XXREAL_0:2;
then D . n2 < D . (i + 1) by A406, XXREAL_0:2;
hence contradiction by A197, A402, A405, GOBOARD2:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A410: Sum (lower_volume g,MD2) = Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))

proof

lower_volume g,MD2 = mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)

proof

A411: len (lower_volume g,MD2) = ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A315, A396, INTEGRA1:def 8;
A412: indx D2,D1,j <= len H₂(D2) by A227, INTEGRA1:def 8;
A413: (indx D2,D1,n1) + 1 <= indx D2,D1,j by A225, A393, XXREAL_0:2;
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 A227, A392, A395, A412, JORDAN3:27;
then A414: len (lower_volume g,MD2) = len (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) by A225, A393, A411, XREAL_1:235, XXREAL_0:2;
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 A415: ( 1 <= k & k <= len (lower_volume g,MD2) ) ; :: thesis:
then A416: k in Seg (len (lower_volume g,MD2)) by FINSEQ_1:3;
then A417: k in Seg (len MD2) by INTEGRA1:def 8;
then B417: k in dom MD2 by FINSEQ_1:def 3;
A418: divset MD2,k = [.(lower_bound (divset MD2,k)),(upper_bound (divset MD2,k)).] by INTEGRA1:5;
A419: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k = H₂(D2) . ((k + ((indx D2,D1,n1) + 1)) - 1) by A392, A411, A412, A413, A415, A416, JORDAN3:31;
k <= (indx D2,D1,j) - (((indx D2,D1,n1) + 1) - 1) by A315, A396, A415, INTEGRA1:def 8;
then k + (((indx D2,D1,n1) + 1) - 1) <= indx D2,D1,j by XREAL_1:21;
then A420: (k + ((indx D2,D1,n1) + 1)) - 1 <= len H₂(D2) by A412, XXREAL_0:2;
1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
then 1 + 1 <= k + ((indx D2,D1,n1) + 1) by A415, XREAL_1:9;
then A421: 1 <= (k + ((indx D2,D1,n1) + 1)) - 1 by XREAL_1:21;
consider k2 being Element of NAT such that
A422: (indx D2,D1,n1) + 1 = 1 + k2 ;
k + k2 in Seg (len H₂(D2)) by A420, A421, A422, FINSEQ_1:3;
then A423: k + k2 in Seg (len D2) by INTEGRA1:def 8;
then k + k2 in dom D2 by FINSEQ_1:def 3;
then A424: (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 A419, A422, INTEGRA1:def 8;
( 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 A204, A415, A422, XREAL_1:9;
then A425: k + k2 > 1 by NAT_1:13;
A426: k in dom MD2 by A417, FINSEQ_1:def 3;
A427: k + k2 in dom D2 by A423, FINSEQ_1:def 3;

per cases ;

suppose A428: k = 1 ; :: thesis:

then ( lower_bound (divset MD2,k) = lower_bound B & upper_bound (divset MD2,k) = MD2 . k ) by A426, INTEGRA1:def 5;
then A429: ( lower_bound (divset MD2,k) = D1 . n1 & upper_bound (divset MD2,k) = D2 . ((k + ((indx D2,D1,n1) + 1)) - 1) ) by A225, A227, A294, A392, A396, A411, A415, A416, JORDAN3:31;
( lower_bound (divset D2,(k + k2)) = D2 . ((k + k2) - 1) & upper_bound (divset D2,(k + k2)) = D2 . (k + k2) ) by A425, A427, 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 A20, A202, A422, A428, A429, INTEGRA1:def 21; :: thesis:

end;

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

then A431: ( k - 1 in dom MD2 & k - 1 in NAT ) by A426, INTEGRA1:9;
then A432: 1 <= k - 1 by Lm1;
A433: k - 1 <= ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A411, A415, XREAL_1:148, XXREAL_0:2;
( lower_bound (divset MD2,k) = MD2 . (k - 1) & upper_bound (divset MD2,k) = MD2 . k ) by A426, A430, INTEGRA1:def 5;
then ( lower_bound (divset MD2,k) = D2 . (((k - 1) + ((indx D2,D1,n1) + 1)) - 1) & upper_bound (divset MD2,k) = D2 . ((k + ((indx D2,D1,n1) + 1)) - 1) ) by A225, A227, A294, A392, A396, A411, A415, A416, A431, A432, A433, 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 A422, A425, A427, INTEGRA1:def 5; :: thesis:

end;

then A434: divset MD2,k = divset D2,(k + k2) by A418, INTEGRA1:5;
rng (f | (divset D2,(k + k2))) = rng (g | (divset D2,(k + k2)))

proof

k in dom MD2 by A417, FINSEQ_1:def 3;
then divset D2,(k + k2) c= B by A434, INTEGRA1:10;
hence rng (f | (divset D2,(k + k2))) = rng (g | (divset D2,(k + k2))) by FUNCT_1:82; :: thesis:

end;

hence (lower_volume g,MD2) . k = (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k by A424, A434, B417, INTEGRA1:def 8; :: thesis:

end;

hence lower_volume g,MD2 = mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j) by A414, FINSEQ_1:18; :: thesis:

end;

hence Sum (lower_volume g,MD2) = Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) ; :: thesis:

end;

Sum (lower_volume g,MD1) = Sum (mid H₂(D1),(n1 + 1),j)

proof

A435: len (lower_volume g,MD1) = len MD1 by INTEGRA1:def 8
.= (j -' (n1 + 1)) + 1 by A217, A220, A221, A294, JORDAN3:27
.= (j - (n1 + 1)) + 1 by A217, XREAL_1:235 ;
A436: n1 + 1 <= len H₂(D1) by A221, INTEGRA1:def 8;
A437: j <= len H₂(D1) by A220, INTEGRA1:def 8;
then A438: len (mid H₂(D1),(n1 + 1),j) = (j -' (n1 + 1)) + 1 by A217, A220, A221, A436, JORDAN3:27
.= (j - (n1 + 1)) + 1 by A217, XREAL_1:235 ;
lower_volume g,MD1 = mid H₂(D1),(n1 + 1),j

proof

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 A439: ( 1 <= k & k <= len (lower_volume g,MD1) ) ; :: thesis:
then A440: k in Seg (len (lower_volume g,MD1)) by FINSEQ_1:3;
then A441: k in Seg (len MD1) by INTEGRA1:def 8;
then k in dom MD1 by FINSEQ_1:def 3;
then A442: (lower_volume g,MD1) . k = (lower_bound (rng (g | (divset MD1,k)))) * (vol (divset MD1,k)) by INTEGRA1:def 8;
k <= j - ((n1 + 1) - 1) by A435, A439;
then A443: k + ((n1 + 1) - 1) <= j by XREAL_1:21;
consider k2 being Element of NAT such that
A444: n1 + 1 = 1 + k2 ;
A445: k2 = (n1 + 1) - 1 by A444;
A446: 1 <= k + k2 by A439, NAT_1:12;
k + k2 <= len D1 by A220, A443, A444, XXREAL_0:2;
then A447: k + k2 in Seg (len D1) by A446, FINSEQ_1:3;
then B447: k + k2 in dom D1 by FINSEQ_1:def 3;
A448: (mid H₂(D1),(n1 + 1),j) . k = H₂(D1) . ((k + (n1 + 1)) - 1) by A217, A221, A435, A437, A439, A440, JORDAN3:31
.= (lower_bound (rng (f | (divset D1,(k + k2))))) * (vol (divset D1,(k + k2))) by A444, B447, INTEGRA1:def 8 ;
1 + 1 <= k + k2 by A220, A439, A444, XREAL_1:9;
then A449: 1 < k + k2 by NAT_1:13;
A450: divset MD1,k = [.(lower_bound (divset MD1,k)),(upper_bound (divset MD1,k)).] by INTEGRA1:5;
A451: k in dom MD1 by A441, FINSEQ_1:def 3;
A452: k + k2 in dom D1 by A447, FINSEQ_1:def 3;
A453: divset D1,(k + k2) = divset MD1,k

proof

( 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 A454: k = 1 ; :: thesis:

then ( lower_bound (divset MD1,k) = lower_bound B & upper_bound (divset MD1,k) = MD1 . k ) by A451, INTEGRA1:def 5;
then ( lower_bound (divset MD1,k) = D1 . n1 & upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) ) by A217, A220, A221, A294, A435, A439, A440, 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 A445, A449, A452, A454, INTEGRA1:def 5; :: thesis:

end;

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

then A456: ( k - 1 in dom MD1 & k - 1 in NAT ) by A451, INTEGRA1:9;
then A457: 1 <= k - 1 by Lm1;
A458: k - 1 <= (j - (n1 + 1)) + 1 by A435, A439, XREAL_1:148, XXREAL_0:2;
( lower_bound (divset MD1,k) = MD1 . (k - 1) & upper_bound (divset MD1,k) = MD1 . k ) by A451, A455, INTEGRA1:def 5;
then ( lower_bound (divset MD1,k) = D1 . (((k - 1) + (n1 + 1)) - 1) & upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) ) by A217, A220, A221, A294, A435, A439, A440, A456, A457, A458, 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 A444, A449, A452, INTEGRA1:def 5; :: thesis:

end;

hence divset D1,(k + k2) = divset MD1,k by A450, INTEGRA1:5; :: thesis:

end;

k in dom MD1 by A441, FINSEQ_1:def 3;
then divset D1,(k + k2) c= B by A453, INTEGRA1:10;
hence (lower_volume g,MD1) . k = (mid H₂(D1),(n1 + 1),j) . k by A442, A448, A453, FUNCT_1:82; :: thesis:

end;

hence lower_volume g,MD1 = mid H₂(D1),(n1 + 1),j by A435, A438, FINSEQ_1:18; :: thesis:

end;

hence Sum (lower_volume g,MD1) = Sum (mid H₂(D1),(n1 + 1),j) ; :: 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) by A373, A390, A410, 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;

A459: 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)))

proof

A460: indx D2,D1,n1 < indx D2,D1,j by A225, A228, XXREAL_0:2;
indx D2,D1,j in Seg (len D2) by A224, FINSEQ_1:def 3;
then indx D2,D1,j in Seg (len H₂(D2)) by INTEGRA1:def 8;
then B461: indx D2,D1,j in dom H₂(D2) by FINSEQ_1:def 3;
A462: indx D2,D1,j <= len H₂(D2) by A227, INTEGRA1:def 8;
indx D2,D1,n1 in Seg (len D2) by A203, FINSEQ_1:def 3;
then indx D2,D1,n1 in Seg (len H₂(D2)) by INTEGRA1:def 8;
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 A204, 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 A204, A460, A462, INTEGRA2:4
.= Sum (H₂(D2) | (indx D2,D1,j)) by A227, JORDAN3:25 ;
hence 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 B461, INTEGRA1:def 22; :: thesis:

end;

A463: H₁(D1,j) = H₁(D1,n1) + (Sum (mid H₂(D1),(n1 + 1),j))

proof

A464: j <= len H₂(D1) by A220, INTEGRA1:def 8;
then j in Seg (len H₂(D1)) by A220, FINSEQ_1:3;
then B465: j in dom H₂(D1) by FINSEQ_1:def 3;
n1 in Seg (len D1) by A202, FINSEQ_1:def 3;
then n1 in Seg (len H₂(D1)) by INTEGRA1:def 8;
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 A220, 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 A205, A220, A464, INTEGRA2:4
.= Sum (H₂(D1) | j) by A220, JORDAN3:25 ;
hence H₁(D1,j) = H₁(D1,n1) + (Sum (mid H₂(D1),(n1 + 1),j)) by B465, INTEGRA1:def 22; :: thesis:

end;

A466: (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 A202, A230, XREAL_1:9;
(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 A459, A463;
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 A198, A466; :: thesis:

end;

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

end;

A467: for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A42, A194);
i in Seg (len D) by A22, FINSEQ_1:def 3;
then reconsider i = i as non empty Element of NAT by FINSEQ_1:3;
S₁[i] by A467;
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 A22; :: thesis:

end;

len D in dom D by FINSEQ_5:6;
then consider j being Element of NAT such that
A468: ( j in dom D1 & D . (len D) in divset D1,j & H₁(D2, indx D2,D1,j) - H₁(D1,j) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A21;
A469: len D1 in dom D1 by FINSEQ_5:6;
A470: j = len D1

proof

assume A471: j <> len D1 ; :: thesis:
A472: D . (len D) <= upper_bound (divset D1,j) by A468, INTEGRA2:1;
j <= len D1 by A468, FINSEQ_3:27;
then j < len D1 by A471, XXREAL_0:1;
then D1 . j < D1 . (len D1) by A468, A469, SEQM_3:def 1;
then A473: D1 . j < upper_bound A by INTEGRA1:def 2;
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 A468, A473, INTEGRA1:def 5; :: thesis:

end;

suppose j <> 1 ; :: thesis:

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

end;

hence contradiction by A472, INTEGRA1:def 2; :: thesis:

end;

A474: len D2 in dom D2 by FINSEQ_5:6;
A475: ( indx D2,D1,(len D1) in dom D2 & D1 . (len D1) = D2 . (indx D2,D1,(len D1)) ) by A20, A469, INTEGRA1:def 21;
then upper_bound A = D2 . (indx D2,D1,(len D1)) by INTEGRA1:def 2;
then D2 . (len D2) = D2 . (indx D2,D1,(len D1)) by INTEGRA1:def 2;
then indx D2,D1,(len D1) = len D2 by A474, A475, GOBOARD2:19;
then H₁(D2, len D2) - (lower_sum f,D1) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A468, A470, INTEGRA1:45;
hence (lower_sum f,D2) - (lower_sum f,D1) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by INTEGRA1:45; :: 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 A20; :: thesis:

end;

A476: 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 (((lower_sum f,T) . m) - (lower_integral f)) < e

proof

let e be real number ; :: thesis:
assume A477: e > 0 ; :: thesis:
then A478: e / 2 > 0 by XREAL_1:141;
reconsider e = e as Real by XREAL_0:def 1;
A479: lower_integral f = upper_bound (rng (lower_sum_set f)) by INTEGRA1:def 16;
A480: rng (lower_sum_set f) is bounded_above by A1, INTEGRA2:36;
not dom (lower_sum_set f) is empty by INTEGRA1:def 12;
then not rng (lower_sum_set f) is empty by RELAT_1:65;
then consider y being real number such that
A481: ( y in rng (lower_sum_set f) & (lower_integral f) - (e / 2) < y ) by A478, A479, A480, SEQ_4:def 4;
consider D being Division of A such that
A482: ( D in dom (lower_sum_set f) & y = (lower_sum_set f) . D & D . 1 > lower_bound A ) by A3, A481, Lm8;
A483: y = lower_sum f,D by A482, INTEGRA1:def 12;
set p = len D;
set H = upper_bound (rng f);
set h = lower_bound (rng f);
deffunc H₁( Nat) -> Element of REAL = vol (divset D,$1);
consider v being FinSequence of REAL such that
A484: ( len v = len D & ( for j being Nat st j in dom v holds
v . j = H₁(j) ) ) from FINSEQ_2:sch 1();
A485: dom v = Seg (len D) by A484, FINSEQ_1:def 3;
consider v1 being non-decreasing FinSequence of REAL such that
A486: v,v1 are_fiberwise_equipotent by INTEGRA2:3;
defpred S₁[ Nat] means ( $1 in dom v1 & v1 . $1 > 0 );
A487: ex k being Nat st S₁[k]

proof

consider H being Function such that
A488: ( dom H = dom v & rng H = dom v1 & H is one-to-one & v = v1 * H ) by A486, CLASSES1:85;
consider k being Element of NAT such that
A489: ( k in dom D & vol (divset D,k) > 0 ) by A3, Th1;
dom D = Seg (len v) by A484, FINSEQ_1:def 3;
then A490: ( k in dom v & v . k > 0 ) by A484, A489, A485;
then ( H . k in dom v1 & v1 . (H . k) > 0 ) by A488, FUNCT_1:21, FUNCT_1:22;
then reconsider Hk = H . k as Nat ;
S₁[Hk] by A488, A490, FUNCT_1:21, FUNCT_1:22;
hence ex k being Nat st S₁[k] ; :: thesis:

end;

consider k being Nat such that
A491: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A487);
A492: 2 * (len D) > 0 by XREAL_1:131;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm4, XREAL_1:50;
then ((upper_bound (rng f)) - (lower_bound (rng f))) + 1 > 0 + 0 ;
then A493: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A492, 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 A491; :: 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 A477, A493, XREAL_1:141; :: thesis:

end;

then consider n being Element of NAT such that
A494: 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 A5;
A495: for m being Element of NAT st n <= m holds
abs (((lower_sum f,T) . m) - (lower_integral f)) < e

proof

let m be Element of NAT ; :: thesis:
assume A496: n <= m ; :: thesis:
then A497: ( 0 < (delta T) . m & (delta T) . m < min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) ) by A494;
reconsider D1 = T . m as Division of A ;
consider D2 being Division of A such that
A498: ( 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 A14;
f | A is bounded_below by A1;
then lower_sum f,D <= lower_sum f,D2 by A498, INTEGRA1:48;
then A499: (lower_sum f,D) - (lower_sum f,D2) <= 0 by XREAL_1:49;
A500: delta D1 = (delta T) . m by INTEGRA2:def 3;
A501: delta D1 < min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) by A497, INTEGRA2:def 3;
min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) <= v1 . k by XXREAL_0:17;
then A502: delta D1 < v1 . k by A501, XXREAL_0:2;
A503: v1 . 1 > 0

proof

A504: 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 A505: n1 in dom D ; :: thesis:
then A506: 1 <= n1 by FINSEQ_3:27;

per cases by A506, XXREAL_0:1;

suppose A507: n1 = 1 ; :: thesis:

then ( lower_bound (divset D,n1) = lower_bound A & upper_bound (divset D,n1) = D . n1 ) by A505, INTEGRA1:def 5;
then vol (divset D,n1) = (D . n1) - (lower_bound A) by INTEGRA1:def 6;
hence vol (divset D,n1) > 0 by A482, A507, XREAL_1:52; :: thesis:

end;

suppose A508: n1 > 1 ; :: thesis:

then ( lower_bound (divset D,n1) = D . (n1 - 1) & upper_bound (divset D,n1) = D . n1 ) by A505, INTEGRA1:def 5;
then A509: vol (divset D,n1) = (D . n1) - (D . (n1 - 1)) by INTEGRA1:def 6;
A510: n1 - 1 in dom D by A505, A508, INTEGRA1:9;
n1 < n1 + 1 by XREAL_1:31;
then n1 - 1 < n1 by XREAL_1:21;
then D . (n1 - 1) < D . n1 by A505, A510, SEQM_3:def 1;
hence vol (divset D,n1) > 0 by A509, XREAL_1:52; :: thesis:

end;

( 1 <= k & k <= len v1 ) by A491, FINSEQ_3:27;
then 1 <= len v1 by XXREAL_0:2;
then 1 in dom v1 by FINSEQ_3:27;
then A511: v1 . 1 in rng v1 by FUNCT_1:def 5;
rng v = rng v1 by A486, CLASSES1:83;
then consider n1 being Element of NAT such that
A512: ( n1 in dom v & v1 . 1 = v . n1 ) by A511, PARTFUN1:26;
A513: n1 in Seg (len D) by A484, A512, FINSEQ_1:def 3;
A514: v1 . 1 = vol (divset D,n1) by A484, A512;
n1 in dom D by A513, FINSEQ_1:def 3;
hence v1 . 1 > 0 by A504, A514; :: thesis:

end;

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

proof

A515: k = 1

proof

assume A516: k <> 1 ; :: thesis:
A517: len v1 = len v by A486, RFINSEQ:16;
A518: k in Seg (len v1) by A491, FINSEQ_1:def 3;
k in Seg (len v) by A491, A517, FINSEQ_1:def 3;
then A519: ( 1 <= k & k <= len D ) by A484, FINSEQ_1:3;
then A520: k > 1 by A516, XXREAL_0:1;
k <= len v1 by A518, FINSEQ_1:3;
then 1 <= len v1 by A519, XXREAL_0:2;
then 1 in dom v1 by FINSEQ_3:27;
hence contradiction by A491, A503, A520; :: thesis:

end;

( min (rng (upper_volume (chi A,A),D)) in rng (upper_volume (chi A,A),D) & ( for x being Real st x in rng (upper_volume (chi A,A),D) holds
min (rng (upper_volume (chi A,A),D)) <= x ) ) by XXREAL_2:def 7;
then consider m being Element of NAT such that
A521: ( m in dom (upper_volume (chi A,A),D) & min (rng (upper_volume (chi A,A),D)) = (upper_volume (chi A,A),D) . m ) by PARTFUN1:26;
m in Seg (len (upper_volume (chi A,A),D)) by A521, FINSEQ_1:def 3;
then A522: m in Seg (len D) by INTEGRA1:def 7;
then m in dom D by FINSEQ_1:def 3;
then min (rng (upper_volume (chi A,A),D)) = vol (divset D,m) by A521, INTEGRA1:22;
then A523: v . m = min (rng (upper_volume (chi A,A),D)) by A484, A522, A485;
m in dom v by A484, A522, FINSEQ_1:def 3;
then A524: min (rng (upper_volume (chi A,A),D)) in rng v by A523, FUNCT_1:def 5;
A525: rng v = rng v1 by A486, CLASSES1:83;
then consider m1 being Element of NAT such that
A526: ( m1 in dom v1 & min (rng (upper_volume (chi A,A),D)) = v1 . m1 ) by A524, PARTFUN1:26;
m1 >= 1 by A526, FINSEQ_3:27;
then A527: v1 . 1 <= min (rng (upper_volume (chi A,A),D)) by A491, A515, A526, INTEGRA2:2;
v1 . k in rng v1 by A491, FUNCT_1:def 5;
then consider k2 being Element of NAT such that
A528: ( k2 in dom v & v1 . k = v . k2 ) by A525, PARTFUN1:26;
A529: k2 in Seg (len D) by A484, A528, FINSEQ_1:def 3;
then B529: k2 in dom D by FINSEQ_1:def 3;
v1 . k = vol (divset D,k2) by A484, A528;
then A530: v1 . k = (upper_volume (chi A,A),D) . k2 by B529, INTEGRA1:22;
k2 in Seg (len (upper_volume (chi A,A),D)) by A529, INTEGRA1:def 7;
then k2 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then v1 . k in rng (upper_volume (chi A,A),D) by A530, FUNCT_1:def 5;
then v1 . k >= min (rng (upper_volume (chi A,A),D)) by XXREAL_2:def 7;
hence v1 . k = min (rng (upper_volume (chi A,A),D)) by A515, A527, XXREAL_0:1; :: thesis:

end;

then consider D3 being Division of A such that
A531: ( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (lower_sum f,D3) - (lower_sum f,D1) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A18, A502;
A532: (lower_sum f,D2) - (lower_sum f,D1) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A498, A531, Th5;
(upper_bound (rng f)) - (lower_bound (rng f)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) + 1 by XREAL_1:31;
then (len D) * ((upper_bound (rng f)) - (lower_bound (rng f))) <= (len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) by XREAL_1:66;
then ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * ((delta T) . m) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A497, XREAL_1:66;
then A533: (lower_sum f,D2) - (lower_sum f,(T . m)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A500, A532, XXREAL_0:2;
A534: (delta T) . m < min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) by A494, A496;
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)) by XXREAL_0:17;
then (delta T) . m < e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by A534, XXREAL_0:2;
then ((delta T) . m) * ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) < e by A493, XREAL_1:81;
then (((delta T) . m) * ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) * 2 < e ;
then A535: ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) < e / 2 by XREAL_1:83;
set s = lower_integral f;
set sD = lower_sum f,D;
set sD1 = lower_sum f,(T . m);
set sD2 = lower_sum f,D2;
((lower_integral f) - (lower_sum f,(T . m))) + (lower_sum f,(T . m)) < (lower_sum f,D) + (e / 2) by A481, A483, XREAL_1:21;
then A536: (lower_integral f) - (lower_sum f,(T . m)) < ((lower_sum f,D) + (e / 2)) - (lower_sum f,(T . m)) by XREAL_1:22;
((lower_sum f,D) - (lower_sum f,(T . m))) - ((lower_sum f,D2) - (lower_sum f,(T . m))) = (lower_sum f,D) - (lower_sum f,D2) ;
then (lower_sum f,D) - (lower_sum f,(T . m)) <= (lower_sum f,D2) - (lower_sum f,(T . m)) by A499, XREAL_1:52;
then (lower_sum f,D) - (lower_sum f,(T . m)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A533, XXREAL_0:2;
then (lower_sum f,D) - (lower_sum f,(T . m)) < e / 2 by A535, XXREAL_0:2;
then ((lower_sum f,D) - (lower_sum f,(T . m))) + (e / 2) < (e / 2) + (e / 2) by XREAL_1:8;
then (lower_integral f) - (lower_sum f,(T . m)) < e by A536, XXREAL_0:2;
then A537: (lower_integral f) - ((lower_sum f,T) . m) < e by INTEGRA2:def 5;
T . m in divs A by INTEGRA1:def 3;
then A538: T . m in dom (lower_sum_set f) by INTEGRA1:def 12;
(lower_sum f,T) . m = lower_sum f,(T . m) by INTEGRA2:def 5;
then (lower_sum f,T) . m = (lower_sum_set f) . (T . m) by A538, INTEGRA1:def 12;
then (lower_sum f,T) . m in rng (lower_sum_set f) by A538, FUNCT_1:def 5;
then upper_bound (rng (lower_sum_set f)) >= (lower_sum f,T) . m by A480, SEQ_4:def 4;
then lower_integral f >= (lower_sum f,T) . m by INTEGRA1:def 16;
then (lower_integral f) - ((lower_sum f,T) . m) >= 0 by XREAL_1:50;
then abs ((lower_integral f) - ((lower_sum f,T) . m)) < e by A537, ABSVALUE:def 1;
then abs (- ((lower_integral f) - ((lower_sum f,T) . m))) < e by COMPLEX1:138;
hence abs (((lower_sum f,T) . m) - (lower_integral f)) < e ; :: thesis:

end;

take n ; :: thesis:
thus for m being Element of NAT st n <= m holds
abs (((lower_sum f,T) . m) - (lower_integral f)) < e by A495; :: thesis:

end;

hence lower_sum f,T is convergent by SEQ_2:def 6; :: thesis:
hence lim (lower_sum f,T) = lower_integral f by A476, SEQ_2:def 7; :: thesis: