let A be closed-interval Subset of REAL ; :: thesis:
let f be Function of A,REAL ; :: thesis:
let T be DivSequence of A; :: thesis:
assume A1: f | A is bounded ; :: thesis:
assume A2: delta T is convergent_to_0 ; :: thesis:
assume 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;
take n ; :: thesis:
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;
reconsider D = T . m as Division of A ;
i in Seg (len D) by A12, INTEGRA1:def 7;
then i in dom D by FINSEQ_1:def 3;
then delta (T . m) = vol (divset (T . m),i) by A11, INTEGRA1:22;
hence ( 0 < (delta T) . m & (delta T) . m < e ) by A8, A9, A10, INTEGRA1:11, XREAL_1:8; :: thesis:

end;

A13: for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum f,D) - (upper_sum f,D2) & 0 <= (upper_sum f,D1) - (upper_sum f,D2) )

proof

let D, D1 be Division of A; :: thesis:
consider D2 being Division of A such that
A14: ( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) ) by Th3;
A15: f | A is bounded_above by A1;
then A16: (upper_sum f,D) - (upper_sum f,D2) >= 0 by A14, INTEGRA1:47, XREAL_1:50;
(upper_sum f,D1) - (upper_sum f,D2) >= 0 by A14, A15, INTEGRA1:47, XREAL_1:50;
hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum f,D) - (upper_sum f,D2) & 0 <= (upper_sum f,D1) - (upper_sum f,D2) ) by A14, A16; :: thesis:

end;

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

proof

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

proof

consider D2 being Division of A such that
A19: ( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum f,D) - (upper_sum f,D2) & 0 <= (upper_sum f,D1) - (upper_sum f,D2) ) by A13;
(upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

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

proof

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

proof

per cases ;

suppose A28: i = 1 ; :: thesis:

len D in Seg (len D) by FINSEQ_1:5;
then 1 <= len D by FINSEQ_1:3;
then A29: 1 in dom D by FINSEQ_3:27;
then A30: ( 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 A26, A28, XREAL_1:11;
then vol (divset D1,j) >= (upper_bound (divset D,1)) - (lower_bound (divset D,1)) by A27, A30, INTEGRA1:def 6;
then A31: vol (divset D1,j) >= vol (divset D,1) by INTEGRA1:def 6;
vol (divset D1,j) <= delta D1 by A24, Lm6;
then A32: delta D1 >= vol (divset D,1) by A31, XXREAL_0:2;
A33: 1 in Seg (len D) by A29, FINSEQ_1:def 3;
then 1 in Seg (len (upper_volume (chi A,A),D)) by INTEGRA1:def 7;
then A34: 1 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
1 in dom D by A33, FINSEQ_1:def 3;
then vol (divset D,1) = (upper_volume (chi A,A),D) . 1 by 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 A32, 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 A23, INTEGRA1:def 5;
then A37: (upper_bound (divset D1,j)) - (lower_bound (divset D1,j)) >= (upper_bound (divset D,i)) - (lower_bound A) by A26, A27, XREAL_1:11;
D . (i - 1) in A by A23, 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 A24, Lm6;
then A39: delta D1 >= vol (divset D,i) by A38, XXREAL_0:2;
A40: i in Seg (len D) by A23, 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 A18; :: 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₁(D1,j) - H₁(D2, indx D2,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₁(D1,j) - H₁(D2, indx D2,D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

A45: j <> 1 by A22, A43, A44;
then reconsider j1 = j - 1 as Element of NAT by A44, INTEGRA1:9;
A46: ( j - 1 in NAT & j - 1 in dom D1 ) 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 A19, 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 A19, 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 m in Seg (len (D1 | j1)) by A58, FINSEQ_1:3;
then A66: m in dom (D1 | j1) by FINSEQ_1:def 3;
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 A19, 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 A19, 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 A19, 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 A19, A70, INTEGRA1:def 21;
then D2 . (indx D2,D1,k) <= D2 . (indx D2,D1,j1) by A19, 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 A19, 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 A19, 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 A19, 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 A19, 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 (upper_volume f,D1) by INTEGRA1:def 7;
then A95: len ((upper_volume f,D1) | j1) = indx D2,D1,j1 by A94, FINSEQ_1:80;
indx D2,D1,j1 in dom D2 by A19, A46, INTEGRA1:def 21;
then indx D2,D1,j1 <= len D2 by FINSEQ_3:27;
then indx D2,D1,j1 <= len (upper_volume f,D2) by INTEGRA1:def 7;
then A96: len ((upper_volume f,D1) | j1) = len ((upper_volume f,D2) | (indx D2,D1,j1)) by A95, FINSEQ_1:80;
for k being Nat st 1 <= k & k <= len ((upper_volume f,D1) | j1) holds
((upper_volume f,D1) | j1) . k = ((upper_volume f,D2) | (indx D2,D1,j1)) . k

proof

let k be Nat; :: thesis:
assume A97: ( 1 <= k & k <= len ((upper_volume f,D1) | j1) ) ; :: thesis:
A98: len (upper_volume f,D1) = len D1 by INTEGRA1:def 7;
then A99: ( 1 <= k & k <= j1 ) by A50, A97, FINSEQ_1:80;
then A100: k in Seg j1 by FINSEQ_1:3;
k <= len D1 by A50, A99, XXREAL_0:2;
then A101: k in Seg (len D1) by A97, 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 A19, 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;
1 <= k1 by A110, FINSEQ_3:27;
then A112: k1 = indx D2,D1,k1 by A77, A111;
indx D2,D1,k <> 1 by A77, A99, A100, 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, A100, 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 A19, 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 (upper_volume f,D1)) by A50, A98, FINSEQ_1:def 3;
then j1 in dom (upper_volume f,D1) by FINSEQ_1:def 3;
then A114: ((upper_volume f,D1) | j1) . k = (upper_volume f,D1) . k by A100, RFINSEQ:19
.= (upper_bound (rng (f | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by A102, B101, INTEGRA1:def 7 ;
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 (upper_volume f,D2)) by INTEGRA1:def 7;
then A117: indx D2,D1,j1 in dom (upper_volume f,D2) by FINSEQ_1:def 3;
((upper_volume f,D2) | (indx D2,D1,j1)) . k = ((upper_volume f,D2) | (indx D2,D1,j1)) . (indx D2,D1,k) by A77, A99, A100
.= (upper_volume f,D2) . (indx D2,D1,k) by A115, A117, RFINSEQ:19
.= (upper_bound (rng (f | (divset D2,(indx D2,D1,k))))) * (vol (divset D2,(indx D2,D1,k))) by B116, INTEGRA1:def 7 ;
hence ((upper_volume f,D1) | j1) . k = ((upper_volume f,D2) | (indx D2,D1,j1)) . k by A114; :: thesis:

end;

then A118: (upper_volume f,D2) | (indx D2,D1,j1) = (upper_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 (upper_volume f,D2)) by INTEGRA1:def 7;
then B119: indx D2,D1,j1 in dom (upper_volume f,D2) by FINSEQ_1:def 3;
j1 in Seg (len D1) by A50, FINSEQ_1:def 3;
then j1 in Seg (len (upper_volume f,D1)) by INTEGRA1:def 7;
then B120: j1 in dom (upper_volume f,D1) by FINSEQ_1:def 3;
A121: (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 A19, A44, A50, Th7;
hence (indx D2,D1,j1) + 1 <= indx D2,D1,j by NAT_1:13; :: thesis:

end;

A122: H₁(D2, indx D2,D1,j1) = Sum ((upper_volume f,D2) | (indx D2,D1,j1)) by B119, INTEGRA1:def 22
.= H₁(D1,j1) by A118, B120, INTEGRA1:def 22 ;
A123: (Sum (mid (upper_volume f,D1),j,j)) - (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof

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

proof

indx D2,D1,j in dom D2 by A19, 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 (upper_volume f,D2)) by INTEGRA1:def 7;
hence ( 1 <= indx D2,D1,j & indx D2,D1,j <= len (upper_volume f,D2) ) by FINSEQ_1:3; :: thesis:

end;

then A125: ( 1 <= (indx D2,D1,j1) + 1 & (indx D2,D1,j1) + 1 <= len (upper_volume f,D2) ) by A48, A121, 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 A19, A44, INTEGRA1:def 21;
then A130: indx D2,D1,j <= len D2 by FINSEQ_3:27;
A131: ID1 in dom D2

proof

A132: ( 1 <= ID1 & ID1 <= indx D2,D1,j ) by A48, A128, XXREAL_0:2;
then ID1 <= len D2 by A130, XXREAL_0:2;
hence ID1 in dom D2 by A132, FINSEQ_3:27; :: thesis:

end;

A133: ID2 in dom D2

proof

A134: ( indx D2,D1,j1 <= ID2 & ID2 <= len D2 ) by A128, A130, XXREAL_0:2;
then 1 <= ID2 by A48, XXREAL_0:2;
hence ID2 in dom D2 by A134, FINSEQ_3:27; :: thesis:

end;

then A135: ( 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;
A136: ( D2 . ID1 in rng D & D2 . ID2 in rng D )

proof

A137: ( D2 . ID1 in rng D2 & D2 . ID2 in rng D2 ) by A131, A133, FUNCT_1:def 5;
A138: ( D1 . j1 = D2 . (indx D2,D1,j1) & D1 . j = D2 . (indx D2,D1,j) ) by A19, A44, A50, INTEGRA1:def 21;
( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

proof

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

per cases by A139;

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

then consider n being Element of NAT such that
A140: ( 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 A135, XXREAL_0:2;
then ( j1 < n & n < j ) by A44, A50, A138, A140, 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
A141: ( 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 A135, XXREAL_0:2;
then ( j1 < n & n < j ) by A44, A50, A138, A141, 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 A19, A137, XBOOLE_0:def 3; :: thesis:

end;

A142: ( 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 A19, A44, A50, INTEGRA1:def 21; :: thesis:

end;

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

proof

( D2 . (indx D2,D1,j1) <= D2 . ID1 & D2 . ID1 <= D2 . (indx D2,D1,j) ) by A135, XXREAL_0:2;
then D2 . ID1 in divset D1,j by A142, INTEGRA2:1;
hence D2 . ID1 in (rng D) /\ (divset D1,j) by A136, 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 A135, XXREAL_0:2;
then D2 . ID2 in divset D1,j by A142, INTEGRA2:1;
hence D2 . ID2 in (rng D) /\ (divset D1,j) by A136, XBOOLE_0:def 4; :: thesis:

end;

hence contradiction by A18, A44, A128, A131, A133, A143, 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

A144: (indx D2,D1,j) -' ((indx D2,D1,j1) + 1) = (indx D2,D1,j) - ((indx D2,D1,j1) + 1) by A121, 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, A144; :: thesis:

end;

then A145: ( 1 <= len (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) & len (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) <= 2 ) by A121, A124, A125, JORDAN3:27;
( 1 <= j & j <= len D1 ) by A44, FINSEQ_3:27;
then A146: ( 1 <= j & j <= len (upper_volume f,D1) ) by INTEGRA1:def 7;
(j -' j) + 1 = 1 by Lm2;
then A147: len (mid (upper_volume f,D1),j,j) = 1 by A146, JORDAN3:27;
(mid (upper_volume f,D1),j,j) . 1 = (upper_volume f,D1) . j by A146, JORDAN3:27;
then mid (upper_volume f,D1),j,j = <*((upper_volume f,D1) . j)*> by A147, FINSEQ_1:57;
then A148: Sum (mid (upper_volume f,D1),j,j) = (upper_volume f,D1) . j by FINSOP_1:12;
A149: (indx D2,D1,j1) + 1 in Seg (len D2)

proof

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

end;

then B149: (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 B150: j in dom D1 by FINSEQ_1:def 3;

now

per cases by A145, Lm3;

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

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

proof

len (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) = ((indx D2,D1,j) -' ((indx D2,D1,j1) + 1)) + 1 by A121, A124, A125, JORDAN3:27;
then (indx D2,D1,j) - ((indx D2,D1,j1) + 1) = 0 by A121, A151, XREAL_1:235;
hence (indx D2,D1,j1) + 1 = indx D2,D1,j ; :: thesis:

end;

A153: 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 A154: divset D1,j = [.(D2 . (indx D2,D1,j1)),(D2 . (indx D2,D1,j)).] by INTEGRA1:5;
A155: (indx D2,D1,j) - 1 = indx D2,D1,j1 by A152;
A156: indx D2,D1,j in dom D2 by A19, A44, INTEGRA1:def 21;
indx D2,D1,j <> 1 by A48, A152, 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 A155, A156, INTEGRA1:def 5;
hence divset D2,(indx D2,D1,j) = divset D1,j by A154, INTEGRA1:5; :: thesis:

end;

(mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 1 = (upper_volume f,D2) . ((indx D2,D1,j1) + 1) by A124, A125, JORDAN3:27;
then mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j) = <*((upper_volume f,D2) . ((indx D2,D1,j1) + 1))*> by A151, FINSEQ_1:57;
then A157: Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) = (upper_volume f,D2) . ((indx D2,D1,j1) + 1) by FINSOP_1:12
.= (upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by B149, INTEGRA1:def 7
.= Sum (mid (upper_volume f,D1),j,j) by A148, A152, A153, B150, INTEGRA1:def 7 ;
A158: 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 A158;
hence (Sum (mid (upper_volume f,D1),j,j)) - (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A157; :: thesis:

end;

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

A160: (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 1 = (upper_volume f,D2) . ((indx D2,D1,j1) + 1) by A124, A125, JORDAN3:27;
(mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 2 = (upper_volume f,D2) . ((indx D2,D1,j1) + 2)

proof

A161: 2 + ((indx D2,D1,j1) + 1) >= 0 + 1 by XREAL_1:9;
(mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 2 = H₂(D2) . ((2 + ((indx D2,D1,j1) + 1)) -' 1) by A121, A124, A125, A159, JORDAN3:27
.= H₂(D2) . ((2 + ((indx D2,D1,j1) + 1)) - 1) by A161, XREAL_1:235
.= H₂(D2) . ((indx D2,D1,j1) + (1 + 1)) ;
hence (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) . 2 = (upper_volume f,D2) . ((indx D2,D1,j1) + 2) ; :: thesis:

end;

then mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j) = <*((upper_volume f,D2) . ((indx D2,D1,j1) + 1)),((upper_volume f,D2) . ((indx D2,D1,j1) + 2))*> by A159, A160, FINSEQ_1:61;
then A162: Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) = ((upper_volume f,D2) . ((indx D2,D1,j1) + 1)) + ((upper_volume f,D2) . ((indx D2,D1,j1) + 2)) by RVSUM_1:107;
A163: vol (divset D1,j) = (vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))

proof

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

proof

end;

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

proof

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

end;

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

A167: (indx D2,D1,j1) + 2 in dom D2 by A19, A44, A165, INTEGRA1:def 21;
(indx D2,D1,j1) + 1 in Seg (len (upper_volume f,D2)) by A125, FINSEQ_1:3;
then (indx D2,D1,j1) + 1 in Seg (len D2) by INTEGRA1:def 7;
then A168: (indx D2,D1,j1) + 1 in dom D2 by FINSEQ_1:def 3;
A169: (indx D2,D1,j1) + 1 <> 1 by A48, NAT_1:13;
A170: ((indx D2,D1,j1) + 1) + 1 > 1 by A125, NAT_1:13;
A171: ((indx D2,D1,j1) + 2) - 1 = (indx D2,D1,j1) + 1 ;
A172: ((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 A167, A170, A171, 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 A168, A169, A172, 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 A164, A165, 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 A166, 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 A166 ;
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 A173: (upper_volume f,D1) . j = (upper_bound (rng (f | (divset D1,j)))) * ((vol (divset D2,((indx D2,D1,j1) + 1))) + (vol (divset D2,((indx D2,D1,j1) + 2)))) by B150, INTEGRA1:def 7;
A174: vol (divset D2,((indx D2,D1,j1) + 1)) >= 0 by INTEGRA1:11;
A175: vol (divset D2,((indx D2,D1,j1) + 2)) >= 0 by INTEGRA1:11;
A176: (Sum (mid H₂(D1),j,j)) - (Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset D2,((indx D2,D1,j1) + 2))) + (vol (divset D2,((indx D2,D1,j1) + 1))))

proof

A177: indx D2,D1,j in dom D2 by A19, A44, INTEGRA1:def 21;
then indx D2,D1,j in Seg (len D2) by FINSEQ_1:def 3;
then B178: indx D2,D1,j in dom D2 by FINSEQ_1:def 3;
A179: indx D2,D1,j = (indx D2,D1,j1) + 2

proof

end;

set ID1 = (indx D2,D1,j1) + 1;
set ID2 = (indx D2,D1,j1) + 2;
A180: Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) = ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 2))))) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + (H₂(D2) . ((indx D2,D1,j1) + 1)) by A162, A179, B178, INTEGRA1:def 7
.= ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 2))))) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) by B149, INTEGRA1:def 7 ;
divset D2,((indx D2,D1,j1) + 2) c= A by A177, A179, INTEGRA1:10;
then A181: upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 2)))) >= lower_bound (rng f) by A1, Lm5;
(indx D2,D1,j1) + 1 in dom D2 by A149, FINSEQ_1:def 3;
then divset D2,((indx D2,D1,j1) + 1) c= A by INTEGRA1:10;
then upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1)))) >= lower_bound (rng f) by A1, Lm5;
then A182: (upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))) by A174, XREAL_1:66;
divset D1,j c= A by A44, INTEGRA1:10;
then upper_bound (rng (f | (divset D1,j))) <= upper_bound (rng f) by A1, Lm5;
then A183: ( (upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 2))) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2))) & (upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 1))) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))) ) by A174, A175, XREAL_1:66;
set SR = upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))));
set VR = vol (divset D2,((indx D2,D1,j1) + 1));
(Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) - ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2))) by A175, A180, A181, XREAL_1:66;
then Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) >= ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) by XREAL_1:21;
then (Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) - ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) >= (upper_bound (rng (f | (divset D2,((indx D2,D1,j1) + 1))))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by XREAL_1:21;
then (Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) - ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))) by A182, XXREAL_0:2;
then A184: Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j)) >= ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1)))) by XREAL_1:21;
reconsider A = upper_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));
((upper_volume f,D1) . j) - (A * (vol (divset D2,((indx D2,D1,j1) + 1)))) = A * (vol (divset D2,((indx D2,D1,j1) + 2))) by A173;
then Sum (mid H₂(D1),j,j) <= ((upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 1)))) + ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) by A148, A183, XREAL_1:22;
then (Sum (mid H₂(D1),j,j)) - ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) <= (upper_bound (rng (f | (divset D1,j)))) * (vol (divset D2,((indx D2,D1,j1) + 1))) by XREAL_1:22;
then (Sum (mid H₂(D1),j,j)) - ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) <= (upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))) by A183, XXREAL_0:2;
then Sum (mid H₂(D1),j,j) <= ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1)))) by XREAL_1:22;
then (Sum (mid H₂(D1),j,j)) - (Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= (((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((upper_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))))) - (((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 2)))) + ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,j1) + 1))))) by A184, XREAL_1:15;
hence (Sum (mid H₂(D1),j,j)) - (Sum (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset D2,((indx D2,D1,j1) + 2))) + (vol (divset D2,((indx D2,D1,j1) + 1)))) ; :: thesis:

end;

(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, 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 (upper_volume f,D1),j,j)) - (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A163, A176, XXREAL_0:2; :: thesis:

end;

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

end;

A185: H₁(D2, indx D2,D1,j1) + (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) = H₁(D2, indx D2,D1,j)

proof

indx D2,D1,j in dom D2 by A19, A44, INTEGRA1:def 21;
then A186: indx D2,D1,j in Seg (len D2) by FINSEQ_1:def 3;
then A187: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len D2 ) by FINSEQ_1:3;
then A188: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len H₂(D2) ) by INTEGRA1:def 7;
indx D2,D1,j in Seg (len H₂(D2)) by A186, INTEGRA1:def 7;
then B189: indx D2,D1,j in dom H₂(D2) by FINSEQ_1:def 3;
A190: indx D2,D1,j1 < indx D2,D1,j by A121, 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 7;
then indx D2,D1,j1 in dom H₂(D2) by FINSEQ_1:def 3;
then H₁(D2, indx D2,D1,j1) = Sum (H₂(D2) | (indx D2,D1,j1)) by INTEGRA1:def 22;
then H₁(D2, indx D2,D1,j1) + (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) = Sum ((H₂(D2) | (indx D2,D1,j1)) ^ (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) by RVSUM_1:105
.= Sum ((mid H₂(D2),1,(indx D2,D1,j1)) ^ (mid H₂(D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) by A48, JORDAN3:25
.= Sum (mid H₂(D2),1,(indx D2,D1,j)) by A48, A188, A190, INTEGRA2:4
.= Sum (H₂(D2) | (indx D2,D1,j)) by A187, JORDAN3:25 ;
hence H₁(D2, indx D2,D1,j1) + (Sum (mid (upper_volume f,D2),((indx D2,D1,j1) + 1),(indx D2,D1,j))) = H₁(D2, indx D2,D1,j) by B189, INTEGRA1:def 22; :: thesis:

end;

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

proof

A191: j in Seg (len D1) by A44, FINSEQ_1:def 3;
then A192: ( 1 <= j & j <= len D1 ) by FINSEQ_1:3;
then A193: ( 1 <= j & j <= len H₂(D1) ) by INTEGRA1:def 7;
j in Seg (len H₂(D1)) by A191, INTEGRA1:def 7;
then B194: j in dom H₂(D1) by FINSEQ_1:def 3;
j < j + 1 by NAT_1:13;
then A195: 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 7;
then j1 in dom H₂(D1) by FINSEQ_1:def 3;
then H₁(D1,j1) = Sum (H₂(D1) | j1) by INTEGRA1:def 22;
then H₁(D1,j1) + (Sum (mid H₂(D1),j,j)) = Sum ((H₂(D1) | j1) ^ (mid H₂(D1),j,j)) by RVSUM_1:105
.= Sum ((mid H₂(D1),1,j1) ^ (mid H₂(D1),(j1 + 1),j)) by A50, JORDAN3:25
.= Sum (mid H₂(D1),1,j) by A50, A193, A195, INTEGRA2:4
.= Sum (H₂(D1) | j) by A192, JORDAN3:25 ;
hence H₁(D1,j1) + (Sum (mid (upper_volume f,D1),j,j)) = H₁(D1,j) by B194, INTEGRA1:def 22; :: thesis:

end;

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

end;

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

end;

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

proof

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

proof

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

proof

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

now

per cases by A208, XXREAL_0:1;

suppose n1 = j ; :: thesis:

then ( D . i in divset D1,j & D . i in rng D ) by A203, A204, FUNCT_1:def 5;
then A209: D . i in (rng D) /\ (divset D1,j) by XBOOLE_0:def 4;
D . (i + 1) in rng D by A199, FUNCT_1:def 5;
then A210: D . (i + 1) in (rng D) /\ (divset D1,j) by A200, XBOOLE_0:def 4;
i + 1 > i by XREAL_1:31;
hence contradiction by A18, A199, A200, A203, A209, A210, Th4, GOBOARD2:19; :: thesis:

end;

suppose n1 > j ; :: thesis:

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

proof

per cases ;

suppose j = 1 ; :: thesis:

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

end;

suppose j <> 1 ; :: thesis:

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

end;

lower_bound (divset D1,n1) = D1 . (n1 - 1) by A204, A215, INTEGRA1:def 5;
then D . i >= D1 . j by A213, A216, XXREAL_0:2;
then A218: D . i >= D . (i + 1) by A214, A217, XXREAL_0:2;
i < i + 1 by XREAL_1:31;
hence contradiction by A199, A203, A218, SEQM_3:def 1; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then A219: n1 + 1 <= j by NAT_1:13;
then A220: j - n1 >= 1 by XREAL_1:21;
A221: n1 >= 1 by A204, FINSEQ_3:27;
A222: ( 1 <= n1 & 1 <= j & j <= len D1 ) by A200, A204, FINSEQ_3:27;
then A223: ( 1 <= n1 + 1 & n1 + 1 <= len D1 ) by A219, NAT_1:12, XXREAL_0:2;
then A224: n1 + 1 in dom D1 by FINSEQ_3:27;
then A225: ( indx D2,D1,(n1 + 1) in dom D2 & D2 . (indx D2,D1,(n1 + 1)) = D1 . (n1 + 1) ) by A19, INTEGRA1:def 21;
A226: ( indx D2,D1,j in dom D2 & D2 . (indx D2,D1,j) = D1 . j ) by A19, A200, INTEGRA1:def 21;
D1 . (n1 + 1) <= D1 . j by A200, A219, A224, GOBOARD2:18;
then A227: indx D2,D1,(n1 + 1) <= indx D2,D1,j by A225, A226, SEQM_3:def 1;
A228: ( 1 <= indx D2,D1,(n1 + 1) & indx D2,D1,(n1 + 1) <= len D2 ) by A225, FINSEQ_3:27;
A229: ( 1 <= indx D2,D1,j & indx D2,D1,j <= len D2 ) by A226, FINSEQ_3:27;
n1 < n1 + 1 by NAT_1:13;
then D1 . n1 < D1 . (n1 + 1) by A204, A224, SEQM_3:def 1;
then A230: indx D2,D1,n1 < indx D2,D1,(n1 + 1) by A205, A225, GOBOARD2:18;
1 + (indx D2,D1,(n1 + 1)) <= (indx D2,D1,j) + 1 by A227, XREAL_1:8;
then 1 <= ((indx D2,D1,j) + 1) - (indx D2,D1,(n1 + 1)) by XREAL_1:21;
then A231: (mid D2,(indx D2,D1,(n1 + 1)),(indx D2,D1,j)) . 1 = D2 . ((1 - 1) + (indx D2,D1,(n1 + 1))) by A227, A228, A229, JORDAN3:31
.= D1 . (n1 + 1) by A19, A224, INTEGRA1:def 21 ;
A232: (Sum (mid H₂(D1),(n1 + 1),j)) - (Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

proof

per cases by A219, XXREAL_0:1;

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

A234: ( 1 <= n1 + 1 & n1 + 1 <= len H₂(D1) ) by A223, INTEGRA1:def 7;
A235: (j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A233, XREAL_1:235;
n1 + 1 in Seg (len D1) by A224, FINSEQ_1:def 3;
then B236: n1 + 1 in dom D1 by FINSEQ_1:def 3;
A237: len (mid H₂(D1),(n1 + 1),j) = 1 by A233, A234, A235, JORDAN3:27;
(n1 + 1) + 1 <= j + 1 by A219, XREAL_1:8;
then 1 <= (j + 1) - (n1 + 1) by XREAL_1:21;
then (mid H₂(D1),(n1 + 1),j) . 1 = H₂(D1) . ((1 + (n1 + 1)) - 1) by A233, A234, JORDAN3:31
.= (upper_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))) by B236, INTEGRA1:def 7 ;
then mid H₂(D1),(n1 + 1),j = <*((upper_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))))*> by A237, FINSEQ_1:57;
then A238: Sum (mid H₂(D1),(n1 + 1),j) = (upper_bound (rng (f | (divset D1,(n1 + 1))))) * (vol (divset D1,(n1 + 1))) by FINSOP_1:12;
divset D1,(n1 + 1) c= A by A224, INTEGRA1:10;
then A239: upper_bound (rng (f | (divset D1,(n1 + 1)))) <= upper_bound (rng f) by A1, Lm5;
vol (divset D1,(n1 + 1)) >= 0 by INTEGRA1:11;
then A240: Sum (mid H₂(D1),(n1 + 1),j) <= (upper_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A238, A239, XREAL_1:66;
D1 . n1 < D1 . j by A200, A204, A207, SEQM_3:def 1;
then A241: indx D2,D1,n1 < indx D2,D1,j by A205, A226, GOBOARD2:18;
then A242: (indx D2,D1,n1) + 1 <= indx D2,D1,j by NAT_1:13;
then (indx D2,D1,n1) + 1 <= len D2 by A229, XXREAL_0:2;
then A243: (indx D2,D1,n1) + 1 <= len H₂(D2) by INTEGRA1:def 7;
A244: 1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
A245: indx D2,D1,j <= len H₂(D2) by A229, INTEGRA1:def 7;
then A246: len (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) = ((indx D2,D1,j) -' ((indx D2,D1,n1) + 1)) + 1 by A229, A242, A243, A244, JORDAN3:27
.= ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A242, XREAL_1:235
.= (indx D2,D1,j) - (indx D2,D1,n1) ;
A247: (indx D2,D1,j) - (indx D2,D1,n1) <= 2

proof

assume (indx D2,D1,j) - (indx D2,D1,n1) > 2 ; :: thesis:
then A248: (indx D2,D1,n1) + 2 < indx D2,D1,j by XREAL_1:22;
A249: indx D2,D1,n1 < (indx D2,D1,n1) + 1 by NAT_1:13;
A250: (indx D2,D1,n1) + 1 < (indx D2,D1,n1) + 2 by XREAL_1:8;
A251: ( (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 A248, A250, XXREAL_0:2; :: thesis:
then ( 1 <= (indx D2,D1,n1) + 1 & (indx D2,D1,n1) + 1 <= len D2 ) by A206, A229, NAT_1:13, XXREAL_0:2;
hence (indx D2,D1,n1) + 1 in dom D2 by FINSEQ_3:27; :: thesis:

end;

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

proof

A253: D2 . ((indx D2,D1,n1) + 1) in rng D2 by A251, 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
A254: ( 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 A205, A226, A249, A251, SEQM_3:def 1;
then ( n1 < k1 & k1 < j ) by A200, A204, A205, A226, A254, GOBOARD2:18;
hence contradiction by A233, NAT_1:13; :: thesis:

end;

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

end;

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

proof

A256: ( lower_bound (divset D1,j) = D1 . (j - 1) & upper_bound (divset D1,j) = D1 . j ) by A200, A207, A221, 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 A205, A226, A249, A251, GOBOARD2:18;
then D2 . ((indx D2,D1,n1) + 1) in divset D1,j by A205, A226, A233, A256, INTEGRA2:1;
hence D2 . ((indx D2,D1,n1) + 1) in (rng D) /\ (divset D1,j) by A252, XBOOLE_0:def 4; :: thesis:

end;

A257: ( 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 A250, NAT_1:13; :: thesis:
then ( 1 <= (indx D2,D1,n1) + 2 & (indx D2,D1,n1) + 2 <= len D2 ) by A206, A229, A248, XXREAL_0:2;
hence (indx D2,D1,n1) + 2 in dom D2 by FINSEQ_3:27; :: thesis:

end;

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

proof

A259: D2 . ((indx D2,D1,n1) + 2) in rng D2 by A257, 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
A260: ( 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 A205, A226, A248, A257, SEQM_3:def 1;
then ( n1 < k1 & k1 < j ) by A200, A204, A205, A226, A260, GOBOARD2:18;
hence contradiction by A233, NAT_1:13; :: thesis:

end;

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

end;

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

proof

A261: ( lower_bound (divset D1,j) = D1 . (j - 1) & upper_bound (divset D1,j) = D1 . j ) by A200, A207, A221, 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 A205, A226, A248, A257, GOBOARD2:18;
then D2 . ((indx D2,D1,n1) + 2) in divset D1,j by A205, A226, A233, A261, INTEGRA2:1;
hence D2 . ((indx D2,D1,n1) + 2) in (rng D) /\ (divset D1,j) by A258, XBOOLE_0:def 4; :: thesis:

end;

then D2 . ((indx D2,D1,n1) + 1) = D2 . ((indx D2,D1,n1) + 2) by A18, A200, A255, Th4;
hence contradiction by A250, A251, A257, SEQM_3:def 1; :: thesis:

end;

A262: ( (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 A241, NAT_1:13;
then A263: ( (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 A264: ((indx D2,D1,n1) + 1) + 1 <= indx D2,D1,j by NAT_1:13;
(indx D2,D1,n1) + 2 >= indx D2,D1,j by A247, XREAL_1:22;
hence (indx D2,D1,n1) + 2 = indx D2,D1,j by A264, 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 A263; :: thesis:

end;

Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1)))

proof

now

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

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

then 1 = ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 ;
then A266: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 1 = H₂(D2) . ((1 + ((indx D2,D1,n1) + 1)) - 1) by A244, A245, JORDAN3:31
.= H₂(D2) . ((indx D2,D1,n1) + 1) ;
(indx D2,D1,n1) + 1 in Seg (len D2) by A226, A265, FINSEQ_1:def 3;
then (indx D2,D1,n1) + 1 in dom D2 by FINSEQ_1:def 3;
then A267: H₂(D2) . ((indx D2,D1,n1) + 1) = (upper_bound (rng (f | (divset D2,((indx D2,D1,n1) + 1))))) * (vol (divset D2,((indx D2,D1,n1) + 1))) by INTEGRA1:def 7;
A268: divset D2,((indx D2,D1,n1) + 1) = divset D1,(n1 + 1)

proof

A269: 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 + 1 by A206, XREAL_1:8;
then (indx D2,D1,n1) + 1 <> 1 ;
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 A226, A265, INTEGRA1:def 5;
then A270: ( lower_bound (divset D2,((indx D2,D1,n1) + 1)) = D1 . n1 & upper_bound (divset D2,((indx D2,D1,n1) + 1)) = D1 . j ) by A19, A200, A204, A265, INTEGRA1:def 21;
( lower_bound (divset D1,(n1 + 1)) = D1 . ((n1 + 1) - 1) & upper_bound (divset D1,(n1 + 1)) = D1 . (n1 + 1) ) by A207, A221, A224, A233, INTEGRA1:def 5;
hence divset D2,((indx D2,D1,n1) + 1) = divset D1,(n1 + 1) by A233, A269, A270, INTEGRA1:5; :: thesis:

end;

vol (divset D2,((indx D2,D1,n1) + 1)) >= 0 by INTEGRA1:11;
then A271: H₂(D2) . ((indx D2,D1,n1) + 1) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A1, A226, A265, A267, A268, Th18, XREAL_1:66;
mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j) = <*(H₂(D2) . ((indx D2,D1,n1) + 1))*> by A246, A265, A266, FINSEQ_1:57;
hence Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= (lower_bound (rng f)) * (vol (divset D1,(n1 + 1))) by A271, FINSOP_1:12; :: thesis:

end;

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

A273: ((indx D2,D1,n1) + 2) - 1 = (indx D2,D1,n1) + 1 ;
A274: ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 >= 1 by A272;
A275: ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 = 1 + 1 by A272;
A276: ( 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 A229, A272, XXREAL_0:2;
then A277: (indx D2,D1,n1) + 1 in dom D2 by A276, FINSEQ_3:27;
A278: indx D2,D1,j <= len H₂(D2) by A229, INTEGRA1:def 7;
then A279: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . 1 = H₂(D2) . ((1 + ((indx D2,D1,n1) + 1)) - 1) by A272, A274, A276, 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 A275, A276, A278, 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 A246, A272, A279, FINSEQ_1:61;
then A280: 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;
A281: H₂(D2) . ((indx D2,D1,n1) + 1) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1)))

proof

(indx D2,D1,n1) + 1 in Seg (len D2) by A277, FINSEQ_1:def 3;
then (indx D2,D1,n1) + 1 in dom D2 by FINSEQ_1:def 3;
then A282: H₂(D2) . ((indx D2,D1,n1) + 1) = (upper_bound (rng (f | (divset D2,((indx D2,D1,n1) + 1))))) * (vol (divset D2,((indx D2,D1,n1) + 1))) by INTEGRA1:def 7;
vol (divset D2,((indx D2,D1,n1) + 1)) >= 0 by INTEGRA1:11;
hence H₂(D2) . ((indx D2,D1,n1) + 1) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1))) by A1, A277, A282, Th18, XREAL_1:66; :: thesis:

end;

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

proof

(indx D2,D1,n1) + 2 in Seg (len D2) by A226, A272, FINSEQ_1:def 3;
then (indx D2,D1,n1) + 2 in dom D2 by FINSEQ_1:def 3;
then A283: H₂(D2) . ((indx D2,D1,n1) + 2) = (upper_bound (rng (f | (divset D2,((indx D2,D1,n1) + 2))))) * (vol (divset D2,((indx D2,D1,n1) + 2))) by INTEGRA1:def 7;
vol (divset D2,((indx D2,D1,n1) + 2)) >= 0 by INTEGRA1:11;
hence H₂(D2) . ((indx D2,D1,n1) + 2) >= (lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 2))) by A1, A226, A272, A283, Th18, XREAL_1:66; :: thesis:

end;

then A284: Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) >= ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 1)))) + ((lower_bound (rng f)) * (vol (divset D2,((indx D2,D1,n1) + 2)))) by A280, A281, 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 A206, NAT_1:13;
then A285: ( 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 A277, INTEGRA1:def 5;
(indx D2,D1,n1) + 2 >= 2 + 1 by A206, XREAL_1:8;
then (indx D2,D1,n1) + 2 <> 1 ;
then A286: ( 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 A226, A272, A273, INTEGRA1:def 5;
A287: vol (divset D2,((indx D2,D1,n1) + 1)) = (D2 . ((indx D2,D1,n1) + 1)) - (D1 . n1) by A205, A285, INTEGRA1:def 6;
A288: vol (divset D2,((indx D2,D1,n1) + 2)) = (D1 . j) - (D2 . ((indx D2,D1,n1) + 1)) by A226, A286, INTEGRA1:def 6;
( lower_bound (divset D1,(n1 + 1)) = D1 . ((n1 + 1) - 1) & upper_bound (divset D1,(n1 + 1)) = D1 . (n1 + 1) ) by A207, A221, A224, A233, 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 A233, A287, A288; :: thesis:

end;

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

end;

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

end;

then A289: (Sum (mid H₂(D1),(n1 + 1),j)) - (Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) * (vol (divset D1,(n1 + 1)))) - ((lower_bound (rng f)) * (vol (divset D1,(n1 + 1)))) by A240, XREAL_1:15;
A290: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm4, XREAL_1:50;
vol (divset D1,(n1 + 1)) <= delta D1

proof

A291: n1 + 1 in Seg (len D1) by A224, FINSEQ_1:def 3;
then n1 + 1 in dom D1 by FINSEQ_1:def 3;
then A292: 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 A291, INTEGRA1:def 7;
then n1 + 1 in dom (upper_volume (chi A,A),D1) by FINSEQ_1:def 3;
then A293: vol (divset D1,(n1 + 1)) in rng (upper_volume (chi A,A),D1) by A292, 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 A293, 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 A290, XREAL_1:66;
hence (Sum (mid H₂(D1),(n1 + 1),j)) - (Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A289, XXREAL_0:2; :: thesis:

end;

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

A295: n1 < n1 + 1 by NAT_1:13;
then A296: D1 . n1 < D1 . (n1 + 1) by A204, A224, SEQM_3:def 1;
then consider B being closed-interval Subset of REAL , MD1, MD2 being Division of B such that
A297: ( 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 A19, A200, A219, A224, A231, Th14;
A298: len MD1 = (j -' (n1 + 1)) + 1 by A219, A222, A223, A297, JORDAN3:27;
A299: j -' (n1 + 1) = j - (n1 + 1) by A219, XREAL_1:235;
A300: len MD1 = (j - (n1 + 1)) + 1 by A219, A298, XREAL_1:235;
A301: (j -' (n1 + 1)) + 1 = j - n1 by A299;
A302: ((len MD1) + (n1 + 1)) - 1 = j by A300;
A303: B c= A

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis:
assume A304: x1 in B ; :: thesis:
then reconsider x1 = x1 as Real ;
A305: rng D1 c= A by INTEGRA1:def 2;
A306: ( D1 . n1 <= x1 & x1 <= MD1 . (len MD1) ) by A297, A304, INTEGRA2:1;
( D1 . n1 in rng D1 & D1 . j in rng D1 ) by A200, A204, FUNCT_1:def 5;
then A307: ( lower_bound A <= D1 . n1 & D1 . j <= upper_bound A ) by A305, INTEGRA2:1;
MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A219, A220, A222, A223, A297, A298, A299, JORDAN3:31
.= D1 . j ;
then ( lower_bound A <= x1 & x1 <= upper_bound A ) by A306, A307, 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;
A308: g | B is bounded

proof

A309: ( f | A is bounded_above & f | A is bounded_below ) by A1;
then consider a being real number such that
A310: 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 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 A303, XBOOLE_1:26;
then a <= f . x by A310, A312;
hence a <= g . x by A311, FUNCT_1:70; :: thesis:

end;

then A313: g | B is bounded_below by RFUNCT_1:88;
consider a being real number such that
A314: for x being set st x in A /\ (dom f) holds
f . x <= a by A309, 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 A315: x in dom g by XBOOLE_0:def 4;
then A316: x in (dom f) /\ B by RELAT_1:90;
(dom f) /\ B c= (dom f) /\ A by A303, XBOOLE_1:26;
then a >= f . x by A314, A316;
hence g . x <= a by A315, FUNCT_1:70; :: thesis:

end;

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

end;

rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:34;
then A317: 1 <= len MD2 by FINSEQ_3:27;
A318: len MD2 = ((indx D2,D1,j) -' (indx D2,D1,(n1 + 1))) + 1 by A227, A228, A229, A297, JORDAN3:27;
then A319: len MD2 = ((indx D2,D1,j) - (indx D2,D1,(n1 + 1))) + 1 by A227, XREAL_1:235;
then A320: ((len MD2) - 1) + (indx D2,D1,(n1 + 1)) = indx D2,D1,j ;
A321: 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 A322: x1 in rng MD2 ; :: thesis:
then reconsider x1 = x1 as Real ;
A323: ( MD2 . 1 <= x1 & x1 <= MD2 . (len MD2) ) by A322, Th15;
A324: MD2 . 1 = D2 . (indx D2,D1,(n1 + 1)) by A228, A229, A297, JORDAN3:27;
A325: MD2 . (len MD2) = D2 . (indx D2,D1,j) by A227, A228, A229, A297, A317, A318, A320, JORDAN3:31;
A326: ( D1 . (n1 + 1) <= x1 & x1 <= D1 . j ) by A19, A224, A226, A227, A228, A229, A297, A317, A318, A320, A323, A324, INTEGRA1:def 21, JORDAN3:31;
A327: rng MD2 c= rng D2 by A297, JORDAN3:28;

now

per cases by A19, A322, A327, XBOOLE_0:def 3;

suppose x1 in rng D1 ; :: thesis:

then consider k being Element of NAT such that
A328: ( k in dom D1 & D1 . k = x1 ) by PARTFUN1:26;
A329: ( n1 + 1 <= k & k <= j ) by A200, A224, A225, A226, A323, A324, A325, A328, SEQM_3:def 1;
then A330: ( 1 <= k - n1 & k - n1 <= j - n1 ) by XREAL_1:11, XREAL_1:21;
A331: ( 1 <= k - n1 & k - n1 <= len MD1 ) by A298, A301, A329, XREAL_1:11, XREAL_1:21;
A332: (j - (n1 + 1)) + 1 = j - n1 ;
n1 <= n1 + 1 by NAT_1:11;
then n1 <= k by A329, XXREAL_0:2;
then consider n being Nat such that
A333: k = n1 + n by NAT_1:10;
n in dom MD1 by A331, A333, FINSEQ_3:27;
then A334: 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 A219, A222, A223, A297, A330, A332, A333, JORDAN3:31
.= D1 . k ;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by A328, A334, XBOOLE_0:def 3; :: thesis:

end;

suppose x1 in rng D ; :: thesis:

then consider n being Element of NAT such that
A335: ( n in dom D & D . n = x1 ) by PARTFUN1:26;
A336: D . i <= upper_bound (divset D1,n1) by A204, 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 A204, INTEGRA1:def 5; :: thesis:

end;

suppose n1 <> 1 ; :: thesis:

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

end;

then D . i < D1 . (n1 + 1) by A296, A336, XXREAL_0:2;
then D . i < D . n by A225, A323, A324, A335, XXREAL_0:2;
then i < n by A203, A335, GOBOARD2:18;
then i + 1 <= n by NAT_1:13;
then A337: ( i + 1 = n or i + 1 < n ) by XXREAL_0:1;
not i + 1 < n

proof

assume i + 1 < n ; :: thesis:
then A338: D . (i + 1) < D . n by A199, A335, SEQM_3:def 1;
lower_bound (divset D1,j) <= D . (i + 1) by A200, INTEGRA2:1;
then A339: lower_bound (divset D1,j) <= D . n by A338, 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 A200, INTEGRA1:def 5; :: thesis:

end;

suppose j <> 1 ; :: thesis:

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

end;

then ( D . n in rng D & D . n in divset D1,j ) by A326, A335, A339, FUNCT_1:def 5, INTEGRA2:1;
then A340: x1 in (rng D) /\ (divset D1,j) by A335, XBOOLE_0:def 4;
A341: D . (i + 1) in rng D by A199, FUNCT_1:def 5;
consider y1 being Real such that
A342: y1 = D . (i + 1) ;
y1 in (rng D) /\ (divset D1,j) by A200, A341, A342, XBOOLE_0:def 4;
hence contradiction by A18, A200, A335, A338, A340, A342, Th4; :: thesis:

end;

then x1 in {(D . (i + 1))} by A335, A337, 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 A343: 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 A344: x1 in (rng MD1) \/ {(D . (i + 1))} ; :: thesis:
then reconsider x1 = x1 as Real ;

now

per cases by A344, XBOOLE_0:def 3;

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

rng MD1 c= rng D1 by A297, JORDAN3:28;
then A346: x1 in rng D1 by A345;
A347: ( MD1 . 1 <= x1 & x1 <= MD1 . (len MD1) ) by A345, Th15;
rng MD1 <> {} ;
then 1 in dom MD1 by FINSEQ_3:34;
then A348: 1 <= len MD1 by FINSEQ_3:27;
A349: len MD1 = (j -' (n1 + 1)) + 1 by A219, A222, A223, A297, JORDAN3:27;
A350: MD1 . 1 = D1 . (n1 + 1) by A222, A223, A297, JORDAN3:27;
((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A219, A349, XREAL_1:235
.= j ;
then A351: MD1 . (len MD1) = D1 . j by A219, A222, A223, A297, A348, A349, JORDAN3:31;
rng D1 c= rng D2 by A19, INTEGRA1:def 20;
then consider k being Element of NAT such that
A352: ( k in dom D2 & D2 . k = x1 ) by A346, PARTFUN1:26;
A353: ( indx D2,D1,(n1 + 1) <= k & k <= indx D2,D1,j ) by A225, A226, A347, A350, A351, A352, SEQM_3:def 1;
then (indx D2,D1,(n1 + 1)) + 1 <= k + 1 by XREAL_1:8;
then A354: 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 A353, XREAL_1:11;
then A355: (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 A353, NAT_1:12;
then consider n being Nat such that
A356: k + 1 = (indx D2,D1,(n1 + 1)) + n by NAT_1:10;
A357: n in NAT by ORDINAL1:def 13;
n in dom MD2 by A319, A354, A355, A356, FINSEQ_3:27;
then A358: MD2 . n in rng MD2 by FUNCT_1:def 5;
(n + (indx D2,D1,(n1 + 1))) - 1 = k by A356;
hence x1 in rng MD2 by A227, A228, A229, A297, A352, A354, A355, A357, A358, JORDAN3:31; :: thesis:

end;

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

then A359: x1 = D . (i + 1) by TARSKI:def 1;
A360: D . (i + 1) in rng D by A199, FUNCT_1:def 5;
rng D c= rng D2 by A19, INTEGRA1:def 20;
then consider k being Element of NAT such that
A361: ( k in dom D2 & x1 = D2 . k ) by A359, A360, PARTFUN1:26;
( lower_bound (divset D1,j) <= D . (i + 1) & D . (i + 1) <= upper_bound (divset D1,j) ) by A200, INTEGRA2:1;
then A362: ( D1 . (j - 1) <= x1 & x1 <= D1 . j ) by A200, A207, A221, A359, INTEGRA1:def 5;
A363: ( j - 1 in dom D1 & j - 1 in NAT ) by A200, A207, A221, INTEGRA1:9;
reconsider j1 = j - 1 as Element of NAT by A200, A207, A221, INTEGRA1:9;
n1 < j1 by A294, XREAL_1:22;
then n1 + 1 <= j1 by NAT_1:13;
then D1 . (n1 + 1) <= D1 . (j - 1) by A224, A363, GOBOARD2:18;
then ( D2 . (indx D2,D1,(n1 + 1)) <= D2 . k & D2 . k <= D2 . (indx D2,D1,j) ) by A19, A200, A225, A361, A362, INTEGRA1:def 21, XXREAL_0:2;
hence x1 in rng MD2 by A225, A226, A297, A361, 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 A343, XBOOLE_0:def 10; :: thesis:

end;

A364: len MD1 in dom MD1 by FINSEQ_5:6;
then A365: 1 <= len MD1 by FINSEQ_3:27;
A366: ( 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 A367: len MD1 = 1 ; :: thesis:

then A368: ( lower_bound (divset MD1,(len MD1)) = lower_bound B & upper_bound (divset MD1,(len MD1)) = MD1 . (len MD1) ) by A364, INTEGRA1:def 5;
( lower_bound (divset D1,j) = D1 . (j - 1) & upper_bound (divset D1,j) = D1 . j ) by A200, A207, A221, 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 A222, A297, A300, A367, A368, JORDAN3:27; :: thesis:

end;

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

then A370: ( lower_bound (divset MD1,(len MD1)) = MD1 . ((len MD1) - 1) & upper_bound (divset MD1,(len MD1)) = MD1 . (len MD1) ) by A364, INTEGRA1:def 5;
A371: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A298, A299;
( (len MD1) - 1 in dom MD1 & (len MD1) - 1 in NAT ) by A364, A369, INTEGRA1:9;
then A372: (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 A373: lower_bound (divset MD1,(len MD1)) = D1 . (j - 1) by A219, A222, A223, A297, A298, A370, A371, A372, JORDAN3:31;
upper_bound (divset MD1,(len MD1)) = D1 . j by A219, A222, A223, A297, A298, A302, A365, A370, JORDAN3:31;
hence ( lower_bound (divset MD1,(len MD1)) = lower_bound (divset D1,j) & upper_bound (divset MD1,(len MD1)) = upper_bound (divset D1,j) ) by A200, A207, A221, A373, INTEGRA1:def 5; :: thesis:

end;

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

proof

A376: vol B = (upper_bound B) - (D1 . n1) by A297, INTEGRA1:def 6;
A377: len MD1 in dom MD1 by FINSEQ_5:6;
( vol B <> 0 & D . (i + 1) > lower_bound B )

proof

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 A377, INTEGRA1:def 5; :: thesis:

end;

suppose len MD1 <> 1 ; :: thesis:

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

end;

then vol B = (D1 . j) - (D1 . n1) by A200, A207, A221, A297, A366, A376, INTEGRA1:def 5;
hence vol B <> 0 by A200, A204, A207, SEQM_3:def 1; :: thesis:
lower_bound (divset D1,j) <= D . (i + 1) by A200, INTEGRA2:1;
then A378: D1 . (j - 1) <= D . (i + 1) by A200, A207, A221, INTEGRA1:def 5;
A379: n1 < j - 1 by A294, XREAL_1:22;
j - 1 in dom D1 by A200, A207, A221, INTEGRA1:9;
then D1 . n1 < D1 . (j - 1) by A204, A379, SEQM_3:def 1;
hence D . (i + 1) > lower_bound B by A297, A378, XXREAL_0:2; :: thesis:

end;

hence (Sum (upper_volume g,MD1)) - (Sum (upper_volume g,MD2)) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A297, A308, A321, A374, Th13; :: thesis:

end;

A380: 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 A380, SEQ_4:64, SEQ_4:65;
then A381: (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 A381, XREAL_1:66;
then A382: (Sum (upper_volume g,MD1)) - (Sum (upper_volume g,MD2)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A375, 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
A383: ( 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 A383, FINSEQ_1:def 3;
then A384: k in Seg (len MD1) by INTEGRA1:def 7;
then k in dom MD1 by FINSEQ_1:def 3;
then A385: delta MD1 = vol (divset MD1,k) by A383, INTEGRA1:22;
n1 + 1 > 1 by A221, NAT_1:13;
then n1 > 1 - 1 by XREAL_1:21;
then A386: ( 1 <= k & k <= len MD1 & k < k + n1 ) by A384, FINSEQ_1:3, XREAL_1:31;
then A387: 1 < k + n1 by XXREAL_0:2;
A388: k in dom MD1 by A384, FINSEQ_1:def 3;
k + n1 <= j by A298, A301, A386, XREAL_1:21;
then k + n1 <= len D1 by A222, XXREAL_0:2;
then A389: k + n1 in dom D1 by A387, FINSEQ_3:27;
A390: 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 A391: k = 1 ; :: thesis:

then ( lower_bound (divset MD1,k) = lower_bound B & upper_bound (divset MD1,k) = MD1 . k ) by A388, INTEGRA1:def 5;
then A392: ( lower_bound (divset MD1,k) = D1 . n1 & upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) ) by A219, A222, A223, A297, A298, A386, JORDAN3:31;
( lower_bound (divset D1,(k + n1)) = D1 . ((k + n1) - 1) & upper_bound (divset D1,(k + n1)) = D1 . (k + n1) ) by A386, A389, 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 A391, A392; :: thesis:

end;

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

then A394: ( k - 1 in dom MD1 & k - 1 in NAT ) by A388, INTEGRA1:9;
then A395: ( 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 A388, A393, 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 A219, A222, A223, A297, A298, A386, A394, A395, 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 A386, A389, 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;

A396: k + n1 in Seg (len D1) by A389, FINSEQ_1:def 3;
then k + n1 in dom D1 by FINSEQ_1:def 3;
then A397: delta MD1 = (upper_volume (chi A,A),D1) . (k + n1) by A385, A390, INTEGRA1:22;
k + n1 in Seg (len (upper_volume (chi A,A),D1)) by A396, 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 A397, FUNCT_1:def 5;
then delta MD1 <= max (rng (upper_volume (chi A,A),D1)) by XXREAL_2:def 8;
then A398: delta MD1 <= delta D1 by INTEGRA1:def 19;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm4, XREAL_1:50;
then A399: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A398, XREAL_1:66;
A400: indx D2,D1,n1 < (indx D2,D1,n1) + 1 by NAT_1:13;
A401: 1 <= (indx D2,D1,n1) + 1 by A206, NAT_1:13;
D1 . n1 < D1 . (n1 + 1) by A204, A224, A295, SEQM_3:def 1;
then indx D2,D1,n1 < indx D2,D1,(n1 + 1) by A205, A225, GOBOARD2:18;
then A402: (indx D2,D1,n1) + 1 <= indx D2,D1,(n1 + 1) by NAT_1:13;
then A403: (indx D2,D1,n1) + 1 <= len D2 by A228, XXREAL_0:2;
then A404: (indx D2,D1,n1) + 1 <= len H₂(D2) by INTEGRA1:def 7;
A405: indx D2,D1,(n1 + 1) = (indx D2,D1,n1) + 1

proof

assume indx D2,D1,(n1 + 1) <> (indx D2,D1,n1) + 1 ; :: thesis:
then A406: indx D2,D1,(n1 + 1) > (indx D2,D1,n1) + 1 by A402, XXREAL_0:1;
A407: (indx D2,D1,n1) + 1 in dom D2 by A401, A403, FINSEQ_3:27;
then A408: D2 . ((indx D2,D1,n1) + 1) in rng D2 by FUNCT_1:def 5;

now

per cases by A19, A408, XBOOLE_0:def 3;

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

then consider n2 being Element of NAT such that
A409: ( 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 A205, A400, A407, SEQM_3:def 1;
then n1 < n2 by A204, A205, A409, GOBOARD2:18;
then A410: n1 + 1 <= n2 by NAT_1:13;
D1 . n2 < D1 . (n1 + 1) by A225, A406, A407, A409, SEQM_3:def 1;
hence contradiction by A224, A409, A410, GOBOARD2:18; :: thesis:

end;

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

then consider n2 being Element of NAT such that
A411: ( n2 in dom D & D2 . ((indx D2,D1,n1) + 1) = D . n2 ) by PARTFUN1:26;
A412: D1 . n1 < D . n2 by A205, A400, A407, A411, SEQM_3:def 1;
A413: D . i <= upper_bound (divset D1,n1) by A204, 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 A204, INTEGRA1:def 5; :: thesis:

end;

suppose n1 <> 1 ; :: thesis:

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

end;

then D . i < D . n2 by A412, A413, XXREAL_0:2;
then i < n2 by A203, A411, GOBOARD2:18;
then A414: i + 1 <= n2 by NAT_1:13;
A415: D . n2 < D1 . (n1 + 1) by A225, A406, A407, A411, SEQM_3:def 1;
A416: ( j - 1 in dom D1 & j - 1 in NAT ) by A200, A207, A221, INTEGRA1:9;
(n1 + 1) + 1 <= j by A294, NAT_1:13;
then n1 + 1 <= j - 1 by XREAL_1:21;
then A417: D1 . (n1 + 1) <= D1 . (j - 1) by A224, A416, GOBOARD2:18;
A418: lower_bound (divset D1,j) <= D . (i + 1) by A200, INTEGRA2:1;
lower_bound (divset D1,j) = D1 . (j - 1) by A200, A207, A221, INTEGRA1:def 5;
then D1 . (n1 + 1) <= D . (i + 1) by A417, A418, XXREAL_0:2;
then D . n2 < D . (i + 1) by A415, XXREAL_0:2;
hence contradiction by A199, A411, A414, GOBOARD2:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

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

proof

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

proof

A420: len (upper_volume g,MD2) = ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A319, A405, INTEGRA1:def 7;
A421: indx D2,D1,j <= len H₂(D2) by A229, INTEGRA1:def 7;
A422: (indx D2,D1,n1) + 1 <= indx D2,D1,j by A227, A402, 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 A229, A401, A404, A421, JORDAN3:27;
then A423: len (upper_volume g,MD2) = len (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) by A227, A402, A420, XREAL_1:235, XXREAL_0:2;
for k being Nat st 1 <= k & k <= len (upper_volume g,MD2) holds
(upper_volume g,MD2) . k = (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k

proof

let k be Nat; :: thesis:
assume A424: ( 1 <= k & k <= len (upper_volume g,MD2) ) ; :: thesis:
then A425: k in Seg (len (upper_volume g,MD2)) by FINSEQ_1:3;
then A426: k in Seg (len MD2) by INTEGRA1:def 7;
then k in dom MD2 by FINSEQ_1:def 3;
then A427: (upper_volume g,MD2) . k = (upper_bound (rng (g | (divset MD2,k)))) * (vol (divset MD2,k)) by INTEGRA1:def 7;
A428: divset MD2,k = [.(lower_bound (divset MD2,k)),(upper_bound (divset MD2,k)).] by INTEGRA1:5;
A429: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k = H₂(D2) . ((k + ((indx D2,D1,n1) + 1)) - 1) by A401, A420, A421, A422, A424, A425, JORDAN3:31;
k <= (indx D2,D1,j) - (((indx D2,D1,n1) + 1) - 1) by A319, A405, A424, INTEGRA1:def 7;
then k + (((indx D2,D1,n1) + 1) - 1) <= indx D2,D1,j by XREAL_1:21;
then A430: (k + ((indx D2,D1,n1) + 1)) - 1 <= len H₂(D2) by A421, XXREAL_0:2;
1 <= (indx D2,D1,n1) + 1 by NAT_1:12;
then 1 + 1 <= k + ((indx D2,D1,n1) + 1) by A424, XREAL_1:9;
then A431: 1 <= (k + ((indx D2,D1,n1) + 1)) - 1 by XREAL_1:21;
consider k2 being Element of NAT such that
A432: (indx D2,D1,n1) + 1 = 1 + k2 ;
k + k2 in Seg (len H₂(D2)) by A430, A431, A432, FINSEQ_1:3;
then A433: k + k2 in Seg (len D2) by INTEGRA1:def 7;
then k + k2 in dom D2 by FINSEQ_1:def 3;
then A434: (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k = (upper_bound (rng (f | (divset D2,(k + k2))))) * (vol (divset D2,(k + k2))) by A429, A432, INTEGRA1:def 7;
( 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 A206, A424, A432, XREAL_1:9;
then A435: k + k2 > 1 by NAT_1:13;
A436: k in dom MD2 by A426, FINSEQ_1:def 3;
A437: k + k2 in dom D2 by A433, FINSEQ_1:def 3;

per cases ;

suppose A438: k = 1 ; :: thesis:

then A439: ( lower_bound (divset MD2,k) = lower_bound B & upper_bound (divset MD2,k) = MD2 . k ) by A436, INTEGRA1:def 5;
then A440: upper_bound (divset MD2,k) = D2 . ((1 + (indx D2,D1,(n1 + 1))) - 1) by A227, A229, A297, A401, A405, A420, A424, A438, JORDAN3:31
.= D1 . (n1 + 1) by A19, A224, INTEGRA1:def 21 ;
( lower_bound (divset D2,(k + k2)) = D2 . ((1 + k2) - 1) & upper_bound (divset D2,(k + k2)) = D2 . (1 + k2) ) by A435, A437, A438, 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 A19, A204, A224, A297, A405, A432, A439, A440, INTEGRA1:def 21; :: thesis:

end;

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

then A442: ( k - 1 in dom MD2 & k - 1 in NAT ) by A436, INTEGRA1:9;
then A443: 1 <= k - 1 by Lm1;
A444: k - 1 <= ((indx D2,D1,j) - ((indx D2,D1,n1) + 1)) + 1 by A420, A424, XREAL_1:148, XXREAL_0:2;
( lower_bound (divset MD2,k) = MD2 . (k - 1) & upper_bound (divset MD2,k) = MD2 . k ) by A436, A441, 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 A227, A229, A297, A401, A405, A420, A424, A425, A442, A443, A444, 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 A432, A435, A437, INTEGRA1:def 5; :: thesis:

end;

then A445: divset MD2,k = divset D2,(k + k2) by A428, INTEGRA1:5;
k in dom MD2 by A426, FINSEQ_1:def 3;
then divset D2,(k + k2) c= B by A445, INTEGRA1:10;
hence (upper_volume g,MD2) . k = (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)) . k by A427, A434, A445, FUNCT_1:82; :: thesis:

end;

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

end;

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

end;

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

proof

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

proof

A446: (j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A219, XREAL_1:235;
A447: len (upper_volume g,MD1) = len MD1 by INTEGRA1:def 7
.= (j - (n1 + 1)) + 1 by A219, A222, A223, A297, A446, JORDAN3:27 ;
A448: n1 + 1 <= len H₂(D1) by A223, INTEGRA1:def 7;
A449: j <= len H₂(D1) by A222, INTEGRA1:def 7;
then A450: len (upper_volume g,MD1) = len (mid H₂(D1),(n1 + 1),j) by A219, A222, A223, A446, A447, A448, JORDAN3:27;
for k being Nat st 1 <= k & k <= len (upper_volume g,MD1) holds
(upper_volume g,MD1) . k = (mid H₂(D1),(n1 + 1),j) . k

proof

let k be Nat; :: thesis:
assume A451: ( 1 <= k & k <= len (upper_volume g,MD1) ) ; :: thesis:
then A452: k in Seg (len (upper_volume g,MD1)) by FINSEQ_1:3;
then A453: k in Seg (len MD1) by INTEGRA1:def 7;
then k in dom MD1 by FINSEQ_1:def 3;
then A454: (upper_volume g,MD1) . k = (upper_bound (rng (g | (divset MD1,k)))) * (vol (divset MD1,k)) by INTEGRA1:def 7;
k <= j - ((n1 + 1) - 1) by A447, A451;
then A455: k + ((n1 + 1) - 1) <= j by XREAL_1:21;
consider k2 being Element of NAT such that
A456: n1 + 1 = 1 + k2 ;
A457: k2 = (n1 + 1) - 1 by A456;
A458: 1 <= k + k2 by A451, NAT_1:12;
k + k2 <= len D1 by A222, A455, A456, XXREAL_0:2;
then A459: k + k2 in Seg (len D1) by A458, FINSEQ_1:3;
then B459: k + k2 in dom D1 by FINSEQ_1:def 3;
A460: (mid H₂(D1),(n1 + 1),j) . k = H₂(D1) . ((k + (n1 + 1)) - 1) by A219, A223, A447, A449, A451, A452, JORDAN3:31
.= (upper_bound (rng (f | (divset D1,(k + k2))))) * (vol (divset D1,(k + k2))) by A456, B459, INTEGRA1:def 7 ;
A461: divset D1,(k + k2) = divset MD1,k

proof

1 + 1 <= k + k2 by A222, A451, A456, XREAL_1:9;
then A462: 1 < k + k2 by NAT_1:13;
A463: divset MD1,k = [.(lower_bound (divset MD1,k)),(upper_bound (divset MD1,k)).] by INTEGRA1:5;
A464: k in dom MD1 by A453, FINSEQ_1:def 3;
A465: k + k2 in dom D1 by A459, FINSEQ_1:def 3;
( 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 A466: k = 1 ; :: thesis:

then ( lower_bound (divset MD1,k) = lower_bound B & upper_bound (divset MD1,k) = MD1 . k ) by A464, INTEGRA1:def 5;
then ( lower_bound (divset MD1,k) = D1 . n1 & upper_bound (divset MD1,k) = D1 . ((k + (n1 + 1)) - 1) ) by A219, A222, A223, A297, A447, A451, A452, 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 A457, A462, A465, A466, INTEGRA1:def 5; :: thesis:

end;

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

then A468: ( k - 1 in dom MD1 & k - 1 in NAT ) by A464, INTEGRA1:9;
then A469: 1 <= k - 1 by Lm1;
A470: k - 1 <= (j - (n1 + 1)) + 1 by A447, A451, XREAL_1:148, XXREAL_0:2;
( lower_bound (divset MD1,k) = MD1 . (k - 1) & upper_bound (divset MD1,k) = MD1 . k ) by A464, A467, 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 A219, A222, A223, A297, A447, A451, A452, A468, A469, A470, 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 A456, A462, A465, INTEGRA1:def 5; :: thesis:

end;

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

end;

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

end;

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

end;

hence Sum (upper_volume g,MD1) = Sum (mid H₂(D1),(n1 + 1),j) ; :: thesis:

end;

hence (Sum (mid H₂(D1),(n1 + 1),j)) - (Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A382, A399, A419, XXREAL_0:2; :: thesis:

end;

A471: 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

A472: indx D2,D1,n1 < indx D2,D1,j by A227, A230, XXREAL_0:2;
indx D2,D1,j in Seg (len D2) by A226, FINSEQ_1:def 3;
then indx D2,D1,j in Seg (len H₂(D2)) by INTEGRA1:def 7;
then B473: indx D2,D1,j in dom H₂(D2) by FINSEQ_1:def 3;
A474: indx D2,D1,j <= len H₂(D2) by A229, INTEGRA1:def 7;
indx D2,D1,n1 in Seg (len D2) by A205, FINSEQ_1:def 3;
then indx D2,D1,n1 in Seg (len H₂(D2)) by INTEGRA1:def 7;
then indx D2,D1,n1 in dom H₂(D2) by FINSEQ_1:def 3;
then H₁(D2, indx D2,D1,n1) = Sum (H₂(D2) | (indx D2,D1,n1)) by INTEGRA1:def 22
.= Sum (mid H₂(D2),1,(indx D2,D1,n1)) by A206, 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 A206, A472, A474, INTEGRA2:4
.= Sum (H₂(D2) | (indx D2,D1,j)) by A229, 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 B473, INTEGRA1:def 22; :: thesis:

end;

A475: j <= len H₂(D1) by A222, INTEGRA1:def 7;
then j in Seg (len H₂(D1)) by A222, FINSEQ_1:3;
then B476: j in dom H₂(D1) by FINSEQ_1:def 3;
n1 in Seg (len D1) by A204, FINSEQ_1:def 3;
then n1 in Seg (len H₂(D1)) by INTEGRA1:def 7;
then n1 in dom H₂(D1) by FINSEQ_1:def 3;
then H₁(D1,n1) = Sum (H₂(D1) | n1) by INTEGRA1:def 22
.= Sum (mid H₂(D1),1,n1) by A222, 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 A207, A222, A475, INTEGRA2:4
.= Sum (H₂(D1) | j) by A222, JORDAN3:25 ;
then A477: H₁(D1,j) = H₁(D1,n1) + (Sum (mid H₂(D1),(n1 + 1),j)) by B476, INTEGRA1:def 22;
A478: (H₁(D1,n1) - H₁(D2, indx D2,D1,n1)) + ((Sum (mid H₂(D1),(n1 + 1),j)) - (Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)))) <= ((i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)) + (((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)) by A204, A232, XREAL_1:9;
(H₁(D1,n1) - H₁(D2, indx D2,D1,n1)) + ((Sum (mid H₂(D1),(n1 + 1),j)) - (Sum (mid H₂(D2),((indx D2,D1,n1) + 1),(indx D2,D1,j)))) = H₁(D1,j) - H₁(D2, indx D2,D1,j) by A471, A477;
hence ex j being Element of NAT st
( j in dom D1 & D . (i + 1) in divset D1,j & H₁(D1,j) - H₁(D2, indx D2,D1,j) <= ((i + 1) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A200, A478; :: thesis:

end;

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

end;

A479: for k being non empty Nat holds S₁[k] from NAT_1:sch 10(A42, A196);
i in Seg (len D) by A21, FINSEQ_1:def 3;
then reconsider i = i as non empty Element of NAT by FINSEQ_1:3;
S₁[i] by A479;
hence ex j being Element of NAT st
( j in dom D1 & D . i in divset D1,j & H₁(D1,j) - H₁(D2, indx D2,D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A21; :: thesis:

end;

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

proof

assume A483: j <> len D1 ; :: thesis:
A484: D . (len D) <= upper_bound (divset D1,j) by A480, INTEGRA2:1;
j in Seg (len D1) by A480, FINSEQ_1:def 3;
then j <= len D1 by FINSEQ_1:3;
then j < len D1 by A483, XXREAL_0:1;
then D1 . j < D1 . (len D1) by A480, A481, SEQM_3:def 1;
then A485: 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 A480, A485, INTEGRA1:def 5; :: thesis:

end;

suppose j <> 1 ; :: thesis:

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

end;

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

end;

A486: len D2 in dom D2 by FINSEQ_5:6;
indx D2,D1,(len D1) = len D2

proof

A487: ( indx D2,D1,(len D1) in dom D2 & D1 . (len D1) = D2 . (indx D2,D1,(len D1)) ) by A19, A481, 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;
hence indx D2,D1,(len D1) = len D2 by A486, A487, GOBOARD2:19; :: thesis:

end;

then (upper_sum f,D1) - H₁(D2, len D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A480, A482, INTEGRA1:44;
hence (upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by INTEGRA1:44; :: thesis:

end;

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

end;

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

proof

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

proof

consider D3 being Element of divs A such that
A494: ( D3 in dom (upper_sum_set f) & y = (upper_sum_set f) . D3 ) by A493, PARTFUN1:26;
reconsider D3 = D3 as Division of A by INTEGRA1:def 3;
A495: len D3 in Seg (len D3) by FINSEQ_1:5;
then 1 <= len D3 by FINSEQ_1:3;
then 1 in Seg (len D3) by FINSEQ_1:3;
then A497: 1 in dom D3 by FINSEQ_1:def 3;
then B496: 1 in dom D3 ;

per cases ;

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

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

end;

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

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

proof

A500: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;
A501: len D3 in dom D3 by A495, FINSEQ_1:def 3;
vol A >= 0 by INTEGRA1:11;
then (upper_bound A) - (lower_bound A) > 0 by A3, INTEGRA1:def 6;
then A502: upper_bound A > lower_bound A by XREAL_1:49;
then A503: len D3 > 1 by A497, A499, A500, A501, GOBOARD2:18;
then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:36;
A504: ( len D = (len D3) - 1 & ( for m being Element of NAT st m in dom D holds
D . m = D3 . (m + 1) ) ) by A503, RFINSEQ:def 2;
then len D <> 0 by A499, A502, INTEGRA1:def 2;
then reconsider D = D as non empty increasing FinSequence of REAL ;
( rng D c= rng D3 & rng D3 c= A ) by FINSEQ_5:36, INTEGRA1:def 2;
then A506: rng D c= A by XBOOLE_1:1;
A507: (len D) + 1 = len D3 by A504;
A508: len D in Seg (len D) by FINSEQ_1:5;
len D in dom D by FINSEQ_5:6;
then D . (len D) = upper_bound A by A500, A503, A507, RFINSEQ:def 2;
then reconsider D = D as Division of A by A506, INTEGRA1:def 2;
D in divs A by INTEGRA1:def 3;
then A509: D in dom (upper_sum_set f) by INTEGRA1:def 11;
A510: y = (upper_sum_set f) . D

proof

A511: y = upper_sum f,D3 by A494, INTEGRA1:def 11
.= Sum (upper_volume f,D3) by INTEGRA1:def 9
.= Sum (((upper_volume f,D3) | 1) ^ ((upper_volume f,D3) /^ 1)) by RFINSEQ:21 ;
A512: 1 <= len (upper_volume f,D3) by A503, INTEGRA1:def 7;
then A513: len ((upper_volume f,D3) | 1) = 1 by FINSEQ_1:80;
A514: 1 in dom (upper_volume f,D3) by A512, FINSEQ_3:27;
1 in Seg 1 by FINSEQ_1:3;
then ((upper_volume f,D3) | 1) . 1 = (upper_volume f,D3) . 1 by A514, RFINSEQ:19;
then A515: (upper_volume f,D3) | 1 = <*((upper_volume f,D3) . 1)*> by A513, FINSEQ_1:57;
A516: vol (divset D3,1) = (upper_bound (divset D3,1)) - (lower_bound (divset D3,1)) by INTEGRA1:def 6
.= (upper_bound (divset D3,1)) - (lower_bound A) by A497, INTEGRA1:def 5
.= (D3 . 1) - (lower_bound A) by A497, INTEGRA1:def 5
.= 0 by A499 ;
A517: (upper_volume f,D3) . 1 = (upper_bound (rng (f | (divset D3,1)))) * (vol (divset D3,1)) by B496, INTEGRA1:def 7;
(upper_volume f,D3) /^ 1 = upper_volume f,D

proof

A518: 2 -' 1 = 2 - 1 by XREAL_1:235
.= 1 ;
A519: len D3 >= 1 + 1 by A503, NAT_1:13;
then len (upper_volume f,D3) >= 2 by INTEGRA1:def 7;
then A520: mid (upper_volume f,D3),2,(len (upper_volume f,D3)) = (upper_volume f,D3) /^ 1 by A518, JORDAN3:26;
A521: ( 2 <= len (upper_volume f,D3) & 1 <= len (upper_volume f,D3) ) by A503, A519, INTEGRA1:def 7;
then A522: len (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) = ((len (upper_volume f,D3)) -' 2) + 1 by JORDAN3:27
.= ((len D3) -' 2) + 1 by INTEGRA1:def 7
.= ((len D3) - 2) + 1 by A519, XREAL_1:235
.= (len D3) - 1 ;
then A523: len (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) = len (upper_volume f,D) by A504, INTEGRA1:def 7;
for i being Nat st 1 <= i & i <= len (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) holds
(mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_volume f,D) . i

proof

let i be Nat; :: thesis:
A524: i in NAT by ORDINAL1:def 13;
assume A525: ( 1 <= i & i <= len (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) ) ; :: thesis:
then i <= (len (upper_volume f,D3)) - 1 by A522, INTEGRA1:def 7;
then i <= ((len (upper_volume f,D3)) - 2) + 1 ;
then A526: (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_volume f,D3) . ((i + 2) - 1) by A521, A524, A525, JORDAN3:31
.= (upper_volume f,D3) . (i + 1) ;
( 1 <= i + 1 & i + 1 <= len D3 ) by A522, A525, NAT_1:12, XREAL_1:21;
then A527: i + 1 in Seg (len D3) by FINSEQ_1:3;
then i + 1 in dom D3 by FINSEQ_1:def 3;
then A528: (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_bound (rng (f | (divset D3,(i + 1))))) * (vol (divset D3,(i + 1))) by A526, INTEGRA1:def 7;
A529: divset D3,(i + 1) = divset D,i

proof

A530: 1 <> i + 1 by A525, NAT_1:13;
i + 1 in dom D3 by A527, FINSEQ_1:def 3;
then A531: ( upper_bound (divset D3,(i + 1)) = D3 . (i + 1) & lower_bound (divset D3,(i + 1)) = D3 . ((i + 1) - 1) ) by A530, INTEGRA1:def 5;
A532: i in dom D by A504, A522, A525, FINSEQ_3:27;
then A533: D . i = D3 . (i + 1) by A503, RFINSEQ:def 2;

per cases ;

suppose A534: i = 1 ; :: thesis:

then A535: ( lower_bound (divset D,i) = lower_bound A & upper_bound (divset D,i) = D . i ) by A532, INTEGRA1:def 5;
divset D3,(i + 1) = [.(lower_bound A),(D . i).] by A499, A531, A533, A534, INTEGRA1:5;
hence divset D3,(i + 1) = divset D,i by A535, INTEGRA1:5; :: thesis:

end;

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

then A537: ( lower_bound (divset D,i) = D . (i - 1) & upper_bound (divset D,i) = D . i ) by A532, INTEGRA1:def 5;
( i - 1 in dom D & i - 1 in NAT ) by A532, A536, INTEGRA1:9;
then ( i - 1 in dom D & i - 1 is Nat ) ;
then D . (i - 1) = D3 . ((i - 1) + 1) by A503, RFINSEQ:def 2
.= D3 . i ;
then divset D3,(i + 1) = [.(lower_bound (divset D,i)),(upper_bound (divset D,i)).] by A531, A533, A537, INTEGRA1:5;
hence divset D3,(i + 1) = divset D,i by INTEGRA1:5; :: thesis:

end;

i in Seg (len D) by A504, A522, A525, FINSEQ_1:3;
then i in dom D by FINSEQ_1:def 3;
hence (mid (upper_volume f,D3),2,(len (upper_volume f,D3))) . i = (upper_volume f,D) . i by A528, A529, INTEGRA1:def 7; :: thesis:

end;

hence (upper_volume f,D3) /^ 1 = upper_volume f,D by A520, A523, FINSEQ_1:18; :: thesis:

end;

then y = 0 + (Sum (upper_volume f,D)) by A511, A515, A516, A517, RVSUM_1:106
.= upper_sum f,D by INTEGRA1:def 9 ;
hence y = (upper_sum_set f) . D by A509, INTEGRA1:def 11; :: thesis:

end;

1 <= len D by A508, FINSEQ_1:3;
then 1 in dom D by FINSEQ_3:27;
then A538: D . 1 = D3 . (1 + 1) by A503, RFINSEQ:def 2
.= D3 . 2 ;
1 + 1 <= len D3 by A503, NAT_1:13;
then 2 in dom D3 by FINSEQ_3:27;
then D3 . 1 < D3 . 2 by A497, SEQM_3:def 1;
hence ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A499, A509, A510, A538; :: thesis:

end;

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

end;

then consider D being Division of A such that
A539: ( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) ;
A540: y = upper_sum f,D by A539, INTEGRA1:def 11;
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
A541: ( len v = len D & ( for j being Nat st j in dom v holds
v . j = H₁(j) ) ) from FINSEQ_2:sch 1();
A542: dom v = Seg (len D) by A541, FINSEQ_1:def 3;
consider v1 being non-decreasing FinSequence of REAL such that
A543: v,v1 are_fiberwise_equipotent by INTEGRA2:3;
defpred S₁[ Nat] means ( $1 in dom v1 & v1 . $1 > 0 );
A544: ex k being Nat st S₁[k]

proof

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

end;

consider k being Nat such that
A548: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A544);
A549: 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 A550: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A549, 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 A548; :: 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 A489, A550, XREAL_1:141; :: thesis:

end;

then consider n being Element of NAT such that
A551: 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;
A552: for m being Element of NAT st n <= m holds
abs (((upper_sum f,T) . m) - (upper_integral f)) < e

proof

let m be Element of NAT ; :: thesis:
assume A553: n <= m ; :: thesis:
then A554: ( 0 < (delta T) . m & (delta T) . m < min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) ) by A551;
reconsider D1 = T . m as Division of A ;
consider D2 being Division of A such that
A555: ( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum f,D) - (upper_sum f,D2) & 0 <= (upper_sum f,D1) - (upper_sum f,D2) ) by A13;
f | A is bounded_above by A1;
then A556: upper_sum f,D2 <= upper_sum f,D by A555, INTEGRA1:47;
A557: delta D1 = (delta T) . m by 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 A558: delta D1 < v1 . k by A554, A557, XXREAL_0:2;
A559: v1 . 1 > 0

proof

A560: 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 A561: n1 in dom D ; :: thesis:
then A562: 1 <= n1 by FINSEQ_3:27;

per cases by A562, XXREAL_0:1;

suppose A563: n1 = 1 ; :: thesis:

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

end;

suppose A564: n1 > 1 ; :: thesis:

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

end;

( 1 <= k & k <= len v1 ) by A548, FINSEQ_3:27;
then 1 <= len v1 by XXREAL_0:2;
then 1 in dom v1 by FINSEQ_3:27;
then A567: v1 . 1 in rng v1 by FUNCT_1:def 5;
rng v = rng v1 by A543, CLASSES1:83;
then consider n1 being Element of NAT such that
A568: ( n1 in dom v & v1 . 1 = v . n1 ) by A567, PARTFUN1:26;
A569: n1 in Seg (len D) by A541, A568, FINSEQ_1:def 3;
A570: v1 . 1 = vol (divset D,n1) by A541, A568;
n1 in dom D by A569, FINSEQ_1:def 3;
hence v1 . 1 > 0 by A560, A570; :: thesis:

end;

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

proof

A571: k = 1

proof

assume A572: k <> 1 ; :: thesis:
A573: len v1 = len v by A543, RFINSEQ:16;
A574: k in Seg (len v1) by A548, FINSEQ_1:def 3;
k in Seg (len v) by A548, A573, FINSEQ_1:def 3;
then A575: ( 1 <= k & k <= len D ) by A541, FINSEQ_1:3;
then A576: k > 1 by A572, XXREAL_0:1;
k <= len v1 by A574, FINSEQ_1:3;
then 1 <= len v1 by A575, XXREAL_0:2;
then 1 in dom v1 by FINSEQ_3:27;
hence contradiction by A548, A559, A576; :: 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
A577: ( 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 A577, FINSEQ_1:def 3;
then A578: 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 A577, INTEGRA1:22;
then A579: v . m = min (rng (upper_volume (chi A,A),D)) by A541, A578, A542;
m in dom v by A541, A578, FINSEQ_1:def 3;
then A580: min (rng (upper_volume (chi A,A),D)) in rng v by A579, FUNCT_1:def 5;
A581: rng v = rng v1 by A543, CLASSES1:83;
then consider m1 being Element of NAT such that
A582: ( m1 in dom v1 & min (rng (upper_volume (chi A,A),D)) = v1 . m1 ) by A580, PARTFUN1:26;
m1 >= 1 by A582, FINSEQ_3:27;
then A583: v1 . 1 <= min (rng (upper_volume (chi A,A),D)) by A548, A571, A582, INTEGRA2:2;
v1 . k in rng (upper_volume (chi A,A),D)

proof

v1 . k in rng v by A548, A581, FUNCT_1:def 5;
then consider k2 being Element of NAT such that
A584: ( k2 in dom v & v1 . k = v . k2 ) by PARTFUN1:26;
A585: k2 in Seg (len D) by A541, A584, FINSEQ_1:def 3;
then B585: k2 in dom D by FINSEQ_1:def 3;
v1 . k = vol (divset D,k2) by A541, A584;
then A586: v1 . k = (upper_volume (chi A,A),D) . k2 by B585, INTEGRA1:22;
k2 in Seg (len (upper_volume (chi A,A),D)) by A585, INTEGRA1:def 7;
then k2 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
hence v1 . k in rng (upper_volume (chi A,A),D) by A586, FUNCT_1:def 5; :: thesis:

end;

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 A571, A583, XXREAL_0:1; :: thesis:

end;

then consider D3 being Division of A such that
A587: ( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (upper_sum f,D1) - (upper_sum f,D3) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A17, A558;
A588: (upper_sum f,D1) - (upper_sum f,D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A555, A587, 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 A554, XREAL_1:66;
then A589: (upper_sum f,(T . m)) - (upper_sum f,D2) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A557, A588, XXREAL_0:2;
A590: (delta T) . m < min (v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) by A551, A553;
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 A590, XXREAL_0:2;
then ((delta T) . m) * ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) < e by A550, XREAL_1:81;
then (((delta T) . m) * ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) * 2 < e ;
then A591: ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) < e / 2 by XREAL_1:83;
set s = upper_integral f;
set sD = upper_sum f,D;
set sD1 = upper_sum f,(T . m);
set sD2 = upper_sum f,D2;
(((upper_sum f,D) + (upper_sum f,(T . m))) - (upper_sum f,(T . m))) - (upper_integral f) < e / 2 by A493, A540, XREAL_1:21;
then (((upper_sum f,(T . m)) - (upper_integral f)) + (upper_sum f,D)) - (upper_sum f,(T . m)) < e / 2 ;
then ((upper_sum f,(T . m)) - (upper_integral f)) + (upper_sum f,D) < (upper_sum f,(T . m)) + (e / 2) by XREAL_1:21;
then A592: (upper_sum f,(T . m)) - (upper_integral f) < ((upper_sum f,(T . m)) + (e / 2)) - (upper_sum f,D) by XREAL_1:22;
(upper_sum f,(T . m)) - (upper_sum f,D) <= (upper_sum f,(T . m)) - (upper_sum f,D2) by A556, XREAL_1:12;
then (upper_sum f,(T . m)) - (upper_sum f,D) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A589, XXREAL_0:2;
then (upper_sum f,(T . m)) - (upper_sum f,D) < e / 2 by A591, XXREAL_0:2;
then ((upper_sum f,(T . m)) - (upper_sum f,D)) + (e / 2) < (e / 2) + (e / 2) by XREAL_1:8;
then (upper_sum f,(T . m)) - (upper_integral f) < e by A592, XXREAL_0:2;
then A593: ((upper_sum f,T) . m) - (upper_integral f) < e by INTEGRA2:def 4;
T . m in divs A by INTEGRA1:def 3;
then A594: T . m in dom (upper_sum_set f) by INTEGRA1:def 11;
(upper_sum f,T) . m = upper_sum f,(T . m) by INTEGRA2:def 4;
then (upper_sum f,T) . m = (upper_sum_set f) . (T . m) by A594, INTEGRA1:def 11;
then (upper_sum f,T) . m in rng (upper_sum_set f) by A594, FUNCT_1:def 5;
then lower_bound (rng (upper_sum_set f)) <= (upper_sum f,T) . m by A492, SEQ_4:def 5;
then upper_integral f <= (upper_sum f,T) . m by INTEGRA1:def 15;
then ((upper_sum f,T) . m) - (upper_integral f) >= 0 by XREAL_1:50;
hence abs (((upper_sum f,T) . m) - (upper_integral f)) < e by A593, ABSVALUE:def 1; :: thesis:

end;

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

end;

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