let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds

for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded implies for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) )

assume A1: f | A is bounded ; :: thesis: for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

then A5: for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by Th20;

for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

let f be Function of A,REAL; :: thesis: ( f | A is bounded implies for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) )

assume A1: f | A is bounded ; :: thesis: for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

then A5: for D, D1 being Division of A ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) & 0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) ) by Th20;

for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

let D, D1 be Division of A; :: thesis: ( delta D1 < min (rng (upper_volume ((chi (A,A)),D))) implies ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) )

assume A11: delta D1 < min (rng (upper_volume ((chi (A,A)),D))) ; :: thesis: ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) )

assume A11: delta D1 < min (rng (upper_volume ((chi (A,A)),D))) ; :: thesis: ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

ex D2 being Division of A st

( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

proof

consider D2 being Division of A such that

A12: D <= D2 and

A13: D1 <= D2 and

A14: rng D2 = (rng D1) \/ (rng D) and

0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) and

0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) by A5;

(lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

A12: D <= D2 and

A13: D1 <= D2 and

A14: rng D2 = (rng D1) \/ (rng D) and

0 <= (lower_sum (f,D2)) - (lower_sum (f,D)) and

0 <= (lower_sum (f,D2)) - (lower_sum (f,D1)) by A5;

(lower_sum (f,D2)) - (lower_sum (f,D1)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)

proof

deffunc H_{1}( Division of A) -> FinSequence of REAL = lower_volume (f,$1);

deffunc H_{2}( Division of A, Nat) -> set = (PartSums (lower_volume (f,$1))) . $2;

A15: len D2 in dom D2 by FINSEQ_5:6;

A16: for i being Element of NAT st i in dom D holds

ex j being Element of NAT st

( j in dom D1 & D . i in divset (D1,j) & H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

deffunc H

A15: len D2 in dom D2 by FINSEQ_5:6;

A16: for i being Element of NAT st i in dom D holds

ex j being Element of NAT st

( j in dom D1 & D . i in divset (D1,j) & H

proof

defpred S_{1}[ non zero Nat] means ( $1 in dom D implies ex j being Element of NAT st

( j in dom D1 & D . $1 in divset (D1,j) & H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= ($1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) );

let i be Element of NAT ; :: thesis: ( i in dom D implies ex j being Element of NAT st

( j in dom D1 & D . i in divset (D1,j) & H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) )

assume A17: i in dom D ; :: thesis: ex j being Element of NAT st

( j in dom D1 & D . i in divset (D1,j) & H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

then A18: i in Seg (len D) by FINSEQ_1:def 3;

A19: for i, j being Element of NAT st i in dom D & j in dom D1 & D . i in divset (D1,j) holds

j >= 2_{1}[1]

A231: for i being non zero Nat st S_{1}[i] holds

S_{1}[i + 1]

( j in dom D1 & D . $1 in divset (D1,j) & H

let i be Element of NAT ; :: thesis: ( i in dom D implies ex j being Element of NAT st

( j in dom D1 & D . i in divset (D1,j) & H

assume A17: i in dom D ; :: thesis: ex j being Element of NAT st

( j in dom D1 & D . i in divset (D1,j) & H

then A18: i in Seg (len D) by FINSEQ_1:def 3;

A19: for i, j being Element of NAT st i in dom D & j in dom D1 & D . i in divset (D1,j) holds

j >= 2

proof

A40:
S
let i, j be Element of NAT ; :: thesis: ( i in dom D & j in dom D1 & D . i in divset (D1,j) implies j >= 2 )

assume A20: i in dom D ; :: thesis: ( not j in dom D1 or not D . i in divset (D1,j) or j >= 2 )

assume that

A21: j in dom D1 and

A22: D . i in divset (D1,j) ; :: thesis: j >= 2

assume j < 2 ; :: thesis: contradiction

then j < 1 + 1 ;

then A23: j <= 1 by NAT_1:13;

j in Seg (len D1) by A21, FINSEQ_1:def 3;

then j >= 1 by FINSEQ_1:1;

then j = 1 by A23, XXREAL_0:1;

then A24: lower_bound (divset (D1,j)) = lower_bound A by A21, INTEGRA1:def 4;

A25: D . i <= upper_bound (divset (D1,j)) by A22, INTEGRA2:1;

delta D1 >= min (rng (upper_volume ((chi (A,A)),D)))

end;assume A20: i in dom D ; :: thesis: ( not j in dom D1 or not D . i in divset (D1,j) or j >= 2 )

assume that

A21: j in dom D1 and

A22: D . i in divset (D1,j) ; :: thesis: j >= 2

assume j < 2 ; :: thesis: contradiction

then j < 1 + 1 ;

then A23: j <= 1 by NAT_1:13;

j in Seg (len D1) by A21, FINSEQ_1:def 3;

then j >= 1 by FINSEQ_1:1;

then j = 1 by A23, XXREAL_0:1;

then A24: lower_bound (divset (D1,j)) = lower_bound A by A21, INTEGRA1:def 4;

A25: D . i <= upper_bound (divset (D1,j)) by A22, INTEGRA2:1;

delta D1 >= min (rng (upper_volume ((chi (A,A)),D)))

proof
end;

hence
contradiction
by A11; :: thesis: verumper cases
( i = 1 or i <> 1 )
;

end;

suppose A26:
i = 1
; :: thesis: delta D1 >= min (rng (upper_volume ((chi (A,A)),D)))

len D in Seg (len D)
by FINSEQ_1:3;

then 1 <= len D by FINSEQ_1:1;

then A27: 1 in Seg (len D) by FINSEQ_1:1;

then A28: 1 in dom D by FINSEQ_1:def 3;

then A29: lower_bound (divset (D,1)) = lower_bound A by INTEGRA1:def 4;

1 in Seg (len (upper_volume ((chi (A,A)),D))) by A27, INTEGRA1:def 6;

then A30: 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

vol (divset (D,1)) = (upper_volume ((chi (A,A)),D)) . 1 by A28, INTEGRA1:20;

then vol (divset (D,1)) in rng (upper_volume ((chi (A,A)),D)) by A30, FUNCT_1:def 3;

then A31: vol (divset (D,1)) >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;

A32: upper_bound (divset (D,1)) = D . 1 by A28, INTEGRA1:def 4;

(upper_bound (divset (D1,j))) - (lower_bound A) >= (D . 1) - (lower_bound A) by A25, A26, XREAL_1:9;

then vol (divset (D1,j)) >= (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by A24, A29, A32, INTEGRA1:def 5;

then A33: vol (divset (D1,j)) >= vol (divset (D,1)) by INTEGRA1:def 5;

vol (divset (D1,j)) <= delta D1 by A21, Lm5;

then delta D1 >= vol (divset (D,1)) by A33, XXREAL_0:2;

hence delta D1 >= min (rng (upper_volume ((chi (A,A)),D))) by A31, XXREAL_0:2; :: thesis: verum

end;then 1 <= len D by FINSEQ_1:1;

then A27: 1 in Seg (len D) by FINSEQ_1:1;

then A28: 1 in dom D by FINSEQ_1:def 3;

then A29: lower_bound (divset (D,1)) = lower_bound A by INTEGRA1:def 4;

1 in Seg (len (upper_volume ((chi (A,A)),D))) by A27, INTEGRA1:def 6;

then A30: 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

vol (divset (D,1)) = (upper_volume ((chi (A,A)),D)) . 1 by A28, INTEGRA1:20;

then vol (divset (D,1)) in rng (upper_volume ((chi (A,A)),D)) by A30, FUNCT_1:def 3;

then A31: vol (divset (D,1)) >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;

A32: upper_bound (divset (D,1)) = D . 1 by A28, INTEGRA1:def 4;

(upper_bound (divset (D1,j))) - (lower_bound A) >= (D . 1) - (lower_bound A) by A25, A26, XREAL_1:9;

then vol (divset (D1,j)) >= (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by A24, A29, A32, INTEGRA1:def 5;

then A33: vol (divset (D1,j)) >= vol (divset (D,1)) by INTEGRA1:def 5;

vol (divset (D1,j)) <= delta D1 by A21, Lm5;

then delta D1 >= vol (divset (D,1)) by A33, XXREAL_0:2;

hence delta D1 >= min (rng (upper_volume ((chi (A,A)),D))) by A31, XXREAL_0:2; :: thesis: verum

suppose A34:
i <> 1
; :: thesis: delta D1 >= min (rng (upper_volume ((chi (A,A)),D)))

then
D . (i - 1) in A
by A20, INTEGRA1:7;

then A35: lower_bound A <= D . (i - 1) by INTEGRA2:1;

lower_bound (divset (D,i)) = D . (i - 1) by A20, A34, INTEGRA1:def 4;

then A36: (upper_bound (divset (D,i))) - (lower_bound A) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A35, XREAL_1:10;

upper_bound (divset (D,i)) = D . i by A20, A34, INTEGRA1:def 4;

then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound A) by A25, A24, XREAL_1:9;

then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A36, XXREAL_0:2;

then vol (divset (D1,j)) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by INTEGRA1:def 5;

then A37: vol (divset (D1,j)) >= vol (divset (D,i)) by INTEGRA1:def 5;

i in Seg (len D) by A20, FINSEQ_1:def 3;

then i in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then A38: i in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

vol (divset (D,i)) = (upper_volume ((chi (A,A)),D)) . i by A20, INTEGRA1:20;

then vol (divset (D,i)) in rng (upper_volume ((chi (A,A)),D)) by A38, FUNCT_1:def 3;

then A39: vol (divset (D,i)) >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;

vol (divset (D1,j)) <= delta D1 by A21, Lm5;

then delta D1 >= vol (divset (D,i)) by A37, XXREAL_0:2;

hence delta D1 >= min (rng (upper_volume ((chi (A,A)),D))) by A39, XXREAL_0:2; :: thesis: verum

end;then A35: lower_bound A <= D . (i - 1) by INTEGRA2:1;

lower_bound (divset (D,i)) = D . (i - 1) by A20, A34, INTEGRA1:def 4;

then A36: (upper_bound (divset (D,i))) - (lower_bound A) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A35, XREAL_1:10;

upper_bound (divset (D,i)) = D . i by A20, A34, INTEGRA1:def 4;

then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound A) by A25, A24, XREAL_1:9;

then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by A36, XXREAL_0:2;

then vol (divset (D1,j)) >= (upper_bound (divset (D,i))) - (lower_bound (divset (D,i))) by INTEGRA1:def 5;

then A37: vol (divset (D1,j)) >= vol (divset (D,i)) by INTEGRA1:def 5;

i in Seg (len D) by A20, FINSEQ_1:def 3;

then i in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def 6;

then A38: i in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;

vol (divset (D,i)) = (upper_volume ((chi (A,A)),D)) . i by A20, INTEGRA1:20;

then vol (divset (D,i)) in rng (upper_volume ((chi (A,A)),D)) by A38, FUNCT_1:def 3;

then A39: vol (divset (D,i)) >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;

vol (divset (D1,j)) <= delta D1 by A21, Lm5;

then delta D1 >= vol (divset (D,i)) by A37, XXREAL_0:2;

hence delta D1 >= min (rng (upper_volume ((chi (A,A)),D))) by A39, XXREAL_0:2; :: thesis: verum

proof

reconsider i = i as non zero Element of NAT by A18, FINSEQ_1:1;
len D in Seg (len D)
by FINSEQ_1:3;

then 1 <= len D by FINSEQ_1:1;

then A41: 1 in dom D by FINSEQ_3:25;

then consider j being Element of NAT such that

A42: j in dom D1 and

A43: D . 1 in divset (D1,j) by Th3, INTEGRA1:6;

H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)
_{1}[1]
by A42, A43; :: thesis: verum

end;then 1 <= len D by FINSEQ_1:1;

then A41: 1 in dom D by FINSEQ_3:25;

then consider j being Element of NAT such that

A42: j in dom D1 and

A43: D . 1 in divset (D1,j) by Th3, INTEGRA1:6;

H

proof

hence
S
A44:
j <> 1
by A19, A41, A42, A43;

then reconsider j1 = j - 1 as Element of NAT by A42, INTEGRA1:7;

A45: j1 in dom D1 by A42, A44, INTEGRA1:7;

then j1 in Seg (len D1) by FINSEQ_1:def 3;

then j1 in Seg (len (lower_volume (f,D1))) by INTEGRA1:def 7;

then A46: j1 in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;

A47: j - 1 in dom D1 by A42, A44, INTEGRA1:7;

then A48: indx (D2,D1,j1) in dom D2 by A13, INTEGRA1:def 19;

then A49: indx (D2,D1,j1) in Seg (len D2) by FINSEQ_1:def 3;

then A50: 1 <= indx (D2,D1,j1) by FINSEQ_1:1;

then mid (D2,1,(indx (D2,D1,j1))) is increasing by A48, INTEGRA1:35;

then A51: D2 | (indx (D2,D1,j1)) is increasing by A50, FINSEQ_6:116;

j < j + 1 by NAT_1:13;

then j1 < j by XREAL_1:19;

then A52: indx (D2,D1,j1) < indx (D2,D1,j) by A13, A42, A45, Th8;

then A53: (indx (D2,D1,j1)) + 1 <= indx (D2,D1,j) by NAT_1:13;

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

then A131: j1 < j by XREAL_1:19;

indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then A132: indx (D2,D1,j) in Seg (len D2) by FINSEQ_1:def 3;

then A133: 1 <= indx (D2,D1,j) by FINSEQ_1:1;

A134: indx (D2,D1,j1) <= len D2 by A49, FINSEQ_1:1;

then A135: len (D2 | (indx (D2,D1,j1))) = indx (D2,D1,j1) by FINSEQ_1:59;

A136: j1 in Seg (len D1) by A47, FINSEQ_1:def 3;

then A137: j1 <= len D1 by FINSEQ_1:1;

for x1 being object st x1 in rng (D1 | j1) holds

x1 in rng (D2 | (indx (D2,D1,j1)))

A150: 1 <= j1 by A136, FINSEQ_1:1;

lower_bound (divset (D1,j)) <= D . 1 by A43, INTEGRA2:1;

then A151: D1 . j1 <= D . 1 by A42, A44, INTEGRA1:def 4;

for x1 being object st x1 in rng (D2 | (indx (D2,D1,j1))) holds

x1 in rng (D1 | j1)

then A170: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A149, XBOOLE_0:def 10;

mid (D1,1,j1) is increasing by A42, A44, A150, INTEGRA1:7, INTEGRA1:35;

then A171: D1 | j1 is increasing by A150, FINSEQ_6:116;

then A172: D2 | (indx (D2,D1,j1)) = D1 | j1 by A51, A170, Th6;

A173: for k being Element of NAT st 1 <= k & k <= j1 holds

k = indx (D2,D1,k)

((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k

then indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;

then A220: indx (D2,D1,j1) <= len (lower_volume (f,D2)) by INTEGRA1:def 7;

j1 <= len D1 by A47, FINSEQ_3:25;

then A221: j1 <= len (lower_volume (f,D1)) by INTEGRA1:def 7;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A51, A171, A170, Th6;

then indx (D2,D1,j1) = j1 by A137, A135, FINSEQ_1:59;

then len ((lower_volume (f,D1)) | j1) = indx (D2,D1,j1) by A221, FINSEQ_1:59;

then len ((lower_volume (f,D1)) | j1) = len ((lower_volume (f,D2)) | (indx (D2,D1,j1))) by A220, FINSEQ_1:59;

then A222: (lower_volume (f,D2)) | (indx (D2,D1,j1)) = (lower_volume (f,D1)) | j1 by A191, FINSEQ_1:14;

A223: j in Seg (len D1) by A42, FINSEQ_1:def 3;

then A224: 1 <= j by FINSEQ_1:1;

indx (D2,D1,j) in Seg (len H_{1}(D2))
by A132, INTEGRA1:def 7;

then A225: indx (D2,D1,j) in dom H_{1}(D2)
by FINSEQ_1:def 3;

indx (D2,D1,j) <= len D2 by A132, FINSEQ_1:1;

then A226: indx (D2,D1,j) <= len H_{1}(D2)
by INTEGRA1:def 7;

j in Seg (len H_{1}(D1))
by A223, INTEGRA1:def 7;

then A227: j in dom H_{1}(D1)
by FINSEQ_1:def 3;

j <= len D1 by A223, FINSEQ_1:1;

then A228: j <= len H_{1}(D1)
by INTEGRA1:def 7;

j1 in Seg (len D1) by A45, FINSEQ_1:def 3;

then j1 in Seg (len H_{1}(D1))
by INTEGRA1:def 7;

then j1 in dom H_{1}(D1)
by FINSEQ_1:def 3;

then H_{2}(D1,j1) = Sum (H_{1}(D1) | j1)
by INTEGRA1:def 20;

then H_{2}(D1,j1) + (Sum (mid (H_{1}(D1),j,j))) =
Sum ((H_{1}(D1) | j1) ^ (mid (H_{1}(D1),j,j)))
by RVSUM_1:75

.= Sum ((mid (H_{1}(D1),1,j1)) ^ (mid (H_{1}(D1),(j1 + 1),j)))
by A150, FINSEQ_6:116

.= Sum (mid (H_{1}(D1),1,j))
by A150, A228, A131, INTEGRA2:4

.= Sum (H_{1}(D1) | j)
by A224, FINSEQ_6:116
;

then A229: H_{2}(D1,j1) + (Sum (mid ((lower_volume (f,D1)),j,j))) = H_{2}(D1,j)
by A227, INTEGRA1:def 20;

indx (D2,D1,j1) in Seg (len D2) by A48, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len H_{1}(D2))
by INTEGRA1:def 7;

then indx (D2,D1,j1) in dom H_{1}(D2)
by FINSEQ_1:def 3;

then H_{2}(D2, indx (D2,D1,j1)) = Sum (H_{1}(D2) | (indx (D2,D1,j1)))
by INTEGRA1:def 20;

then H_{2}(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) =
Sum ((H_{1}(D2) | (indx (D2,D1,j1))) ^ (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))))
by RVSUM_1:75

.= Sum ((mid (H_{1}(D2),1,(indx (D2,D1,j1)))) ^ (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))))
by A50, FINSEQ_6:116

.= Sum (mid (H_{1}(D2),1,(indx (D2,D1,j))))
by A50, A52, A226, INTEGRA2:4

.= Sum (H_{1}(D2) | (indx (D2,D1,j)))
by A133, FINSEQ_6:116
;

then A230: H_{2}(D2, indx (D2,D1,j1)) + (Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) = H_{2}(D2, indx (D2,D1,j))
by A225, INTEGRA1:def 20;

indx (D2,D1,j1) in Seg (len D2) by A48, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len (lower_volume (f,D2))) by INTEGRA1:def 7;

then indx (D2,D1,j1) in dom (lower_volume (f,D2)) by FINSEQ_1:def 3;

then H_{2}(D2, indx (D2,D1,j1)) =
Sum ((lower_volume (f,D2)) | (indx (D2,D1,j1)))
by INTEGRA1:def 20

.= H_{2}(D1,j1)
by A222, A46, INTEGRA1:def 20
;

hence H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)
by A54, A230, A229; :: thesis: verum

end;then reconsider j1 = j - 1 as Element of NAT by A42, INTEGRA1:7;

A45: j1 in dom D1 by A42, A44, INTEGRA1:7;

then j1 in Seg (len D1) by FINSEQ_1:def 3;

then j1 in Seg (len (lower_volume (f,D1))) by INTEGRA1:def 7;

then A46: j1 in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;

A47: j - 1 in dom D1 by A42, A44, INTEGRA1:7;

then A48: indx (D2,D1,j1) in dom D2 by A13, INTEGRA1:def 19;

then A49: indx (D2,D1,j1) in Seg (len D2) by FINSEQ_1:def 3;

then A50: 1 <= indx (D2,D1,j1) by FINSEQ_1:1;

then mid (D2,1,(indx (D2,D1,j1))) is increasing by A48, INTEGRA1:35;

then A51: D2 | (indx (D2,D1,j1)) is increasing by A50, FINSEQ_6:116;

j < j + 1 by NAT_1:13;

then j1 < j by XREAL_1:19;

then A52: indx (D2,D1,j1) < indx (D2,D1,j) by A13, A42, A45, Th8;

then A53: (indx (D2,D1,j1)) + 1 <= indx (D2,D1,j) by NAT_1:13;

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

proof

j < j + 1
by NAT_1:13;
A55:
(indx (D2,D1,j)) - (indx (D2,D1,j1)) <= 2

j <= len D1 by A42, FINSEQ_3:25;

then A83: j <= len (lower_volume (f,D1)) by INTEGRA1:def 7;

A84: 1 <= j by A42, FINSEQ_3:25;

then A85: (mid ((lower_volume (f,D1)),j,j)) . 1 = (lower_volume (f,D1)) . j by A83, FINSEQ_6:118;

reconsider lv = (lower_volume (f,D1)) . j as Element of REAL by XREAL_0:def 1;

(j -' j) + 1 = 1 by Lm1;

then len (mid ((lower_volume (f,D1)),j,j)) = 1 by A84, A83, FINSEQ_6:118;

then mid ((lower_volume (f,D1)),j,j) = <*lv*> by A85, FINSEQ_1:40;

then A86: Sum (mid ((lower_volume (f,D1)),j,j)) = (lower_volume (f,D1)) . j by FINSOP_1:11;

indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then A87: indx (D2,D1,j) in Seg (len D2) by FINSEQ_1:def 3;

then A88: 1 <= indx (D2,D1,j) by FINSEQ_1:1;

indx (D2,D1,j) in Seg (len (lower_volume (f,D2))) by A87, INTEGRA1:def 7;

then A89: indx (D2,D1,j) <= len (lower_volume (f,D2)) by FINSEQ_1:1;

then A90: (indx (D2,D1,j1)) + 1 <= len (lower_volume (f,D2)) by A53, XXREAL_0:2;

then (indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (f,D2))) by A82, FINSEQ_1:1;

then A91: (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

then A92: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;

(indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1) = (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) by A53, XREAL_1:233;

then ((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 <= 2 by A55;

then A93: len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= 2 by A53, A88, A89, A82, A90, FINSEQ_6:118;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 >= 0 + 1 by XREAL_1:6;

then A94: 1 <= len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) by A53, A88, A89, A82, A90, FINSEQ_6:118;

end;proof

A82:
1 <= (indx (D2,D1,j1)) + 1
by A50, NAT_1:13;
reconsider ID1 = (indx (D2,D1,j1)) + 1 as Element of NAT ;

reconsider ID2 = ID1 + 1 as Element of NAT ;

assume (indx (D2,D1,j)) - (indx (D2,D1,j1)) > 2 ; :: thesis: contradiction

then A56: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,j) by XREAL_1:20;

A57: ID1 < ID2 by NAT_1:13;

then indx (D2,D1,j1) <= ID2 by NAT_1:13;

then A58: 1 <= ID2 by A50, XXREAL_0:2;

A59: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then A60: indx (D2,D1,j) <= len D2 by FINSEQ_3:25;

then ID2 <= len D2 by A56, XXREAL_0:2;

then ID2 in Seg (len D2) by A58, FINSEQ_1:1;

then A61: ID2 in dom D2 by FINSEQ_1:def 3;

then A62: D2 . ID2 < D2 . (indx (D2,D1,j)) by A56, A59, SEQM_3:def 1;

A63: 1 <= ID1 by A50, NAT_1:13;

A64: D1 . j = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

ID1 <= indx (D2,D1,j) by A56, A57, XXREAL_0:2;

then ID1 <= len D2 by A60, XXREAL_0:2;

then ID1 in Seg (len D2) by A63, FINSEQ_1:1;

then A65: ID1 in dom D2 by FINSEQ_1:def 3;

then A66: D2 . ID1 < D2 . ID2 by A57, A61, SEQM_3:def 1;

indx (D2,D1,j1) < ID1 by NAT_1:13;

then A67: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A48, A65, SEQM_3:def 1;

A68: D1 . j1 = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

A69: ( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

then A77: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;

then A78: lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

D2 . ID2 in (rng D) \/ (rng D1) by A14, A61, FUNCT_1:def 3;

then A79: D2 . ID2 in rng D by A69, XBOOLE_0:def 3;

D2 . ID1 in (rng D) \/ (rng D1) by A14, A65, FUNCT_1:def 3;

then A80: D2 . ID1 in rng D by A69, XBOOLE_0:def 3;

D2 . (indx (D2,D1,j1)) <= D2 . ID2 by A67, A66, XXREAL_0:2;

then D2 . ID2 in divset (D1,j) by A62, A78, A77, INTEGRA2:1;

then A81: D2 . ID2 in (rng D) /\ (divset (D1,j)) by A79, XBOOLE_0:def 4;

D2 . ID1 <= D2 . (indx (D2,D1,j)) by A66, A62, XXREAL_0:2;

then D2 . ID1 in divset (D1,j) by A67, A78, A77, INTEGRA2:1;

then D2 . ID1 in (rng D) /\ (divset (D1,j)) by A80, XBOOLE_0:def 4;

hence contradiction by A11, A42, A57, A65, A61, A81, Th5, SEQ_4:138; :: thesis: verum

end;reconsider ID2 = ID1 + 1 as Element of NAT ;

assume (indx (D2,D1,j)) - (indx (D2,D1,j1)) > 2 ; :: thesis: contradiction

then A56: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,j) by XREAL_1:20;

A57: ID1 < ID2 by NAT_1:13;

then indx (D2,D1,j1) <= ID2 by NAT_1:13;

then A58: 1 <= ID2 by A50, XXREAL_0:2;

A59: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then A60: indx (D2,D1,j) <= len D2 by FINSEQ_3:25;

then ID2 <= len D2 by A56, XXREAL_0:2;

then ID2 in Seg (len D2) by A58, FINSEQ_1:1;

then A61: ID2 in dom D2 by FINSEQ_1:def 3;

then A62: D2 . ID2 < D2 . (indx (D2,D1,j)) by A56, A59, SEQM_3:def 1;

A63: 1 <= ID1 by A50, NAT_1:13;

A64: D1 . j = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

ID1 <= indx (D2,D1,j) by A56, A57, XXREAL_0:2;

then ID1 <= len D2 by A60, XXREAL_0:2;

then ID1 in Seg (len D2) by A63, FINSEQ_1:1;

then A65: ID1 in dom D2 by FINSEQ_1:def 3;

then A66: D2 . ID1 < D2 . ID2 by A57, A61, SEQM_3:def 1;

indx (D2,D1,j1) < ID1 by NAT_1:13;

then A67: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A48, A65, SEQM_3:def 1;

A68: D1 . j1 = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

A69: ( not D2 . ID1 in rng D1 & not D2 . ID2 in rng D1 )

proof

upper_bound (divset (D1,j)) = D1 . j
by A42, A44, INTEGRA1:def 4;
assume A70:
( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 )
; :: thesis: contradiction

end;per cases
( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 )
by A70;

end;

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

then consider n being Element of NAT such that

A71: n in dom D1 and

A72: D1 . n = D2 . ID1 by PARTFUN1:3;

j1 < n by A45, A67, A68, A71, A72, SEQ_4:137;

then A73: j < n + 1 by XREAL_1:19;

D2 . ID1 < D2 . (indx (D2,D1,j)) by A66, A62, XXREAL_0:2;

then n < j by A42, A64, A71, A72, SEQ_4:137;

hence contradiction by A73, NAT_1:13; :: thesis: verum

end;A71: n in dom D1 and

A72: D1 . n = D2 . ID1 by PARTFUN1:3;

j1 < n by A45, A67, A68, A71, A72, SEQ_4:137;

then A73: j < n + 1 by XREAL_1:19;

D2 . ID1 < D2 . (indx (D2,D1,j)) by A66, A62, XXREAL_0:2;

then n < j by A42, A64, A71, A72, SEQ_4:137;

hence contradiction by A73, NAT_1:13; :: thesis: verum

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

then consider n being Element of NAT such that

A74: n in dom D1 and

A75: D1 . n = D2 . ID2 by PARTFUN1:3;

D2 . (indx (D2,D1,j1)) < D2 . ID2 by A67, A66, XXREAL_0:2;

then j1 < n by A45, A68, A74, A75, SEQ_4:137;

then A76: j < n + 1 by XREAL_1:19;

n < j by A42, A62, A64, A74, A75, SEQ_4:137;

hence contradiction by A76, NAT_1:13; :: thesis: verum

end;A74: n in dom D1 and

A75: D1 . n = D2 . ID2 by PARTFUN1:3;

D2 . (indx (D2,D1,j1)) < D2 . ID2 by A67, A66, XXREAL_0:2;

then j1 < n by A45, A68, A74, A75, SEQ_4:137;

then A76: j < n + 1 by XREAL_1:19;

n < j by A42, A62, A64, A74, A75, SEQ_4:137;

hence contradiction by A76, NAT_1:13; :: thesis: verum

then A77: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;

then A78: lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

D2 . ID2 in (rng D) \/ (rng D1) by A14, A61, FUNCT_1:def 3;

then A79: D2 . ID2 in rng D by A69, XBOOLE_0:def 3;

D2 . ID1 in (rng D) \/ (rng D1) by A14, A65, FUNCT_1:def 3;

then A80: D2 . ID1 in rng D by A69, XBOOLE_0:def 3;

D2 . (indx (D2,D1,j1)) <= D2 . ID2 by A67, A66, XXREAL_0:2;

then D2 . ID2 in divset (D1,j) by A62, A78, A77, INTEGRA2:1;

then A81: D2 . ID2 in (rng D) /\ (divset (D1,j)) by A79, XBOOLE_0:def 4;

D2 . ID1 <= D2 . (indx (D2,D1,j)) by A66, A62, XXREAL_0:2;

then D2 . ID1 in divset (D1,j) by A67, A78, A77, INTEGRA2:1;

then D2 . ID1 in (rng D) /\ (divset (D1,j)) by A80, XBOOLE_0:def 4;

hence contradiction by A11, A42, A57, A65, A61, A81, Th5, SEQ_4:138; :: thesis: verum

j <= len D1 by A42, FINSEQ_3:25;

then A83: j <= len (lower_volume (f,D1)) by INTEGRA1:def 7;

A84: 1 <= j by A42, FINSEQ_3:25;

then A85: (mid ((lower_volume (f,D1)),j,j)) . 1 = (lower_volume (f,D1)) . j by A83, FINSEQ_6:118;

reconsider lv = (lower_volume (f,D1)) . j as Element of REAL by XREAL_0:def 1;

(j -' j) + 1 = 1 by Lm1;

then len (mid ((lower_volume (f,D1)),j,j)) = 1 by A84, A83, FINSEQ_6:118;

then mid ((lower_volume (f,D1)),j,j) = <*lv*> by A85, FINSEQ_1:40;

then A86: Sum (mid ((lower_volume (f,D1)),j,j)) = (lower_volume (f,D1)) . j by FINSOP_1:11;

indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then A87: indx (D2,D1,j) in Seg (len D2) by FINSEQ_1:def 3;

then A88: 1 <= indx (D2,D1,j) by FINSEQ_1:1;

indx (D2,D1,j) in Seg (len (lower_volume (f,D2))) by A87, INTEGRA1:def 7;

then A89: indx (D2,D1,j) <= len (lower_volume (f,D2)) by FINSEQ_1:1;

then A90: (indx (D2,D1,j1)) + 1 <= len (lower_volume (f,D2)) by A53, XXREAL_0:2;

then (indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (f,D2))) by A82, FINSEQ_1:1;

then A91: (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

then A92: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;

(indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1) = (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) by A53, XREAL_1:233;

then ((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 <= 2 by A55;

then A93: len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= 2 by A53, A88, A89, A82, A90, FINSEQ_6:118;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 >= 0 + 1 by XREAL_1:6;

then A94: 1 <= len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) by A53, A88, A89, A82, A90, FINSEQ_6:118;

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

hence
(Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid ((lower_volume (f,D1)),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
; :: thesis: verumper cases
( len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = 1 or len (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = 2 )
by A94, A93, Lm2;

end;

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

upper_bound (divset (D1,j)) = D1 . j
by A42, A44, INTEGRA1:def 4;

then A96: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;

then lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

then A97: divset (D1,j) = [.(D2 . (indx (D2,D1,j1))),(D2 . (indx (D2,D1,j))).] by A96, INTEGRA1:4;

A98: delta D1 >= 0 by Th9;

A99: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;

A100: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 1 by A53, A88, A89, A82, A90, A95, FINSEQ_6:118;

then A101: (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) = 0 by A53, XREAL_1:233;

then indx (D2,D1,j) <> 1 by A49, FINSEQ_1:1;

then A102: upper_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j)) by A100, INTEGRA1:def 4;

(indx (D2,D1,j)) - 1 = indx (D2,D1,j1) by A101;

then lower_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j1)) by A50, A101, A100, INTEGRA1:def 4;

then A103: divset (D2,(indx (D2,D1,j))) = divset (D1,j) by A97, A102, INTEGRA1:4;

reconsider lv = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) as Element of REAL by XREAL_0:def 1;

(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by A88, A89, A82, A90, FINSEQ_6:118;

then mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*lv*> by A95, FINSEQ_1:40;

then Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by FINSOP_1:11

.= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A92, INTEGRA1:def 7

.= Sum (mid ((lower_volume (f,D1)),j,j)) by A42, A86, A101, A103, INTEGRA1:def 7 ;

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

end;then A96: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;

then lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

then A97: divset (D1,j) = [.(D2 . (indx (D2,D1,j1))),(D2 . (indx (D2,D1,j))).] by A96, INTEGRA1:4;

A98: delta D1 >= 0 by Th9;

A99: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;

A100: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 1 by A53, A88, A89, A82, A90, A95, FINSEQ_6:118;

then A101: (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) = 0 by A53, XREAL_1:233;

then indx (D2,D1,j) <> 1 by A49, FINSEQ_1:1;

then A102: upper_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j)) by A100, INTEGRA1:def 4;

(indx (D2,D1,j)) - 1 = indx (D2,D1,j1) by A101;

then lower_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j1)) by A50, A101, A100, INTEGRA1:def 4;

then A103: divset (D2,(indx (D2,D1,j))) = divset (D1,j) by A97, A102, INTEGRA1:4;

reconsider lv = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) as Element of REAL by XREAL_0:def 1;

(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by A88, A89, A82, A90, FINSEQ_6:118;

then mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*lv*> by A95, FINSEQ_1:40;

then Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by FINSOP_1:11

.= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A92, INTEGRA1:def 7

.= Sum (mid ((lower_volume (f,D1)),j,j)) by A42, A86, A101, A103, INTEGRA1:def 7 ;

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

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

A105:
(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)
by A88, A89, A82, A90, FINSEQ_6:118;

A106: 2 + ((indx (D2,D1,j1)) + 1) >= 0 + 1 by XREAL_1:7;

(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 2 = H_{1}(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1)
by A53, A88, A89, A82, A90, A104, FINSEQ_6:118

.= H_{1}(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) - 1)
by A106, XREAL_1:233

.= H_{1}(D2) . ((indx (D2,D1,j1)) + (1 + 1))
;

then mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)),((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 2))*> by A104, A105, FINSEQ_1:44;

then A107: Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = ((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)) + ((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 2)) by RVSUM_1:77;

A108: vol (divset (D2,((indx (D2,D1,j1)) + 1))) >= 0 by INTEGRA1:9;

upper_bound (divset (D1,j)) = D1 . j by A42, A44, INTEGRA1:def 4;

then A109: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

A110: vol (divset (D2,((indx (D2,D1,j1)) + 2))) >= 0 by INTEGRA1:9;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, A88, A89, A82, A90, A104, FINSEQ_6:118;

then A111: ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, XREAL_1:233;

then A112: (indx (D2,D1,j1)) + 2 in dom D2 by A13, A42, INTEGRA1:def 19;

lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;

then lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

then A113: vol (divset (D1,j)) = (((D2 . ((indx (D2,D1,j1)) + 2)) - (D2 . ((indx (D2,D1,j1)) + 1))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A109, A111, INTEGRA1:def 5;

(indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (f,D2))) by A82, A90, FINSEQ_1:1;

then (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

then A114: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;

A115: (indx (D2,D1,j1)) + 1 <> 1 by A50, NAT_1:13;

then A116: upper_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . ((indx (D2,D1,j1)) + 1) by A114, INTEGRA1:def 4;

((indx (D2,D1,j1)) + 1) - 1 = (indx (D2,D1,j1)) + 0 ;

then A117: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A114, A115, INTEGRA1:def 4;

A118: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A82, NAT_1:13;

((indx (D2,D1,j1)) + 2) - 1 = (indx (D2,D1,j1)) + 1 ;

then A119: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A112, A118, INTEGRA1:def 4;

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A112, A118, INTEGRA1:def 4;

then vol (divset (D1,j)) = ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A119, A113, INTEGRA1:def 5

.= (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + ((upper_bound (divset (D2,((indx (D2,D1,j1)) + 1)))) - (lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))))) by A117, A116 ;

then A120: vol (divset (D1,j)) = (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by INTEGRA1:def 5;

then A121: (lower_volume (f,D1)) . j = (lower_bound (rng (f | (divset (D1,j))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A42, INTEGRA1:def 7;

A122: (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))

then ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A42, Lm5, XREAL_1:64;

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

end;A106: 2 + ((indx (D2,D1,j1)) + 1) >= 0 + 1 by XREAL_1:7;

(mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 2 = H

.= H

.= H

then mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)),((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 2))*> by A104, A105, FINSEQ_1:44;

then A107: Sum (mid ((lower_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = ((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)) + ((lower_volume (f,D2)) . ((indx (D2,D1,j1)) + 2)) by RVSUM_1:77;

A108: vol (divset (D2,((indx (D2,D1,j1)) + 1))) >= 0 by INTEGRA1:9;

upper_bound (divset (D1,j)) = D1 . j by A42, A44, INTEGRA1:def 4;

then A109: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A13, A42, INTEGRA1:def 19;

A110: vol (divset (D2,((indx (D2,D1,j1)) + 2))) >= 0 by INTEGRA1:9;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, A88, A89, A82, A90, A104, FINSEQ_6:118;

then A111: ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, XREAL_1:233;

then A112: (indx (D2,D1,j1)) + 2 in dom D2 by A13, A42, INTEGRA1:def 19;

lower_bound (divset (D1,j)) = D1 . j1 by A42, A44, INTEGRA1:def 4;

then lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A13, A45, INTEGRA1:def 19;

then A113: vol (divset (D1,j)) = (((D2 . ((indx (D2,D1,j1)) + 2)) - (D2 . ((indx (D2,D1,j1)) + 1))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A109, A111, INTEGRA1:def 5;

(indx (D2,D1,j1)) + 1 in Seg (len (lower_volume (f,D2))) by A82, A90, FINSEQ_1:1;

then (indx (D2,D1,j1)) + 1 in Seg (len D2) by INTEGRA1:def 7;

then A114: (indx (D2,D1,j1)) + 1 in dom D2 by FINSEQ_1:def 3;

A115: (indx (D2,D1,j1)) + 1 <> 1 by A50, NAT_1:13;

then A116: upper_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . ((indx (D2,D1,j1)) + 1) by A114, INTEGRA1:def 4;

((indx (D2,D1,j1)) + 1) - 1 = (indx (D2,D1,j1)) + 0 ;

then A117: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A114, A115, INTEGRA1:def 4;

A118: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A82, NAT_1:13;

((indx (D2,D1,j1)) + 2) - 1 = (indx (D2,D1,j1)) + 1 ;

then A119: lower_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 1) by A112, A118, INTEGRA1:def 4;

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A112, A118, INTEGRA1:def 4;

then vol (divset (D1,j)) = ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (D2 . ((indx (D2,D1,j1)) + 1))) - (D2 . (indx (D2,D1,j1))) by A119, A113, INTEGRA1:def 5

.= (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + ((upper_bound (divset (D2,((indx (D2,D1,j1)) + 1)))) - (lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))))) by A117, A116 ;

then A120: vol (divset (D1,j)) = (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by INTEGRA1:def 5;

then A121: (lower_volume (f,D1)) . j = (lower_bound (rng (f | (divset (D1,j))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A42, INTEGRA1:def 7;

A122: (Sum (mid (H

proof

(upper_bound (rng f)) - (lower_bound (rng f)) >= 0
by A1, Lm3, XREAL_1:48;
set ID2 = (indx (D2,D1,j1)) + 2;

set ID1 = (indx (D2,D1,j1)) + 1;

set B = vol (divset (D2,((indx (D2,D1,j1)) + 1)));

set C = vol (divset (D2,((indx (D2,D1,j1)) + 2)));

divset (D1,j) c= A by A42, INTEGRA1:8;

then A123: lower_bound (rng (f | (divset (D1,j)))) >= lower_bound (rng f) by A1, Lm4;

(indx (D2,D1,j1)) + 1 in dom D2 by A91, FINSEQ_1:def 3;

then divset (D2,((indx (D2,D1,j1)) + 1)) c= A by INTEGRA1:8;

then lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1))))) <= upper_bound (rng f) by A1, Lm4;

then A124: (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A108, XREAL_1:64;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, A88, A89, A82, A90, A104, FINSEQ_6:118;

then A125: ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, XREAL_1:233;

A126: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then divset (D2,((indx (D2,D1,j1)) + 2)) c= A by A125, INTEGRA1:8;

then A127: lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2))))) <= upper_bound (rng f) by A1, Lm4;

reconsider A = lower_bound (rng (f | (divset (D1,j)))) as Real ;

A128: ((lower_volume (f,D1)) . j) - (A * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = A * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A121;

(lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A110, A123, XREAL_1:64;

then Sum (mid (H_{1}(D1),j,j)) >= ((lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))))
by A86, A128, XREAL_1:19;

then A129: (Sum (mid (H_{1}(D1),j,j))) - ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:19;

(lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A108, A123, XREAL_1:64;

then (Sum (mid (H_{1}(D1),j,j))) - ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A129, XXREAL_0:2;

then A130: Sum (mid (H_{1}(D1),j,j)) >= ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:19;

Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) =
((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + (H_{1}(D2) . ((indx (D2,D1,j1)) + 1))
by A107, A126, A125, INTEGRA1:def 7

.= ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A92, INTEGRA1:def 7 ;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))
by A110, A127, XREAL_1:64;

then Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:20;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by XREAL_1:20;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))
by A124, XXREAL_0:2;

then Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
by XREAL_1:20;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),j,j))) <= (((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))) - (((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))))
by A130, XREAL_1:13;

hence (Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),j,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
; :: thesis: verum

end;set ID1 = (indx (D2,D1,j1)) + 1;

set B = vol (divset (D2,((indx (D2,D1,j1)) + 1)));

set C = vol (divset (D2,((indx (D2,D1,j1)) + 2)));

divset (D1,j) c= A by A42, INTEGRA1:8;

then A123: lower_bound (rng (f | (divset (D1,j)))) >= lower_bound (rng f) by A1, Lm4;

(indx (D2,D1,j1)) + 1 in dom D2 by A91, FINSEQ_1:def 3;

then divset (D2,((indx (D2,D1,j1)) + 1)) c= A by INTEGRA1:8;

then lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1))))) <= upper_bound (rng f) by A1, Lm4;

then A124: (lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A108, XREAL_1:64;

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, A88, A89, A82, A90, A104, FINSEQ_6:118;

then A125: ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A53, XREAL_1:233;

A126: indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then divset (D2,((indx (D2,D1,j1)) + 2)) c= A by A125, INTEGRA1:8;

then A127: lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2))))) <= upper_bound (rng f) by A1, Lm4;

reconsider A = lower_bound (rng (f | (divset (D1,j)))) as Real ;

A128: ((lower_volume (f,D1)) . j) - (A * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = A * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A121;

(lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A110, A123, XREAL_1:64;

then Sum (mid (H

then A129: (Sum (mid (H

(lower_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A108, A123, XREAL_1:64;

then (Sum (mid (H

then A130: Sum (mid (H

Sum (mid (H

.= ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A92, INTEGRA1:def 7 ;

then (Sum (mid (H

then Sum (mid (H

then (Sum (mid (H

then (Sum (mid (H

then Sum (mid (H

then (Sum (mid (H

hence (Sum (mid (H

then ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A42, Lm5, XREAL_1:64;

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

then A131: j1 < j by XREAL_1:19;

indx (D2,D1,j) in dom D2 by A13, A42, INTEGRA1:def 19;

then A132: indx (D2,D1,j) in Seg (len D2) by FINSEQ_1:def 3;

then A133: 1 <= indx (D2,D1,j) by FINSEQ_1:1;

A134: indx (D2,D1,j1) <= len D2 by A49, FINSEQ_1:1;

then A135: len (D2 | (indx (D2,D1,j1))) = indx (D2,D1,j1) by FINSEQ_1:59;

A136: j1 in Seg (len D1) by A47, FINSEQ_1:def 3;

then A137: j1 <= len D1 by FINSEQ_1:1;

for x1 being object st x1 in rng (D1 | j1) holds

x1 in rng (D2 | (indx (D2,D1,j1)))

proof

then A149:
rng (D1 | j1) c= rng (D2 | (indx (D2,D1,j1)))
;
let x1 be object ; :: thesis: ( x1 in rng (D1 | j1) implies x1 in rng (D2 | (indx (D2,D1,j1))) )

assume x1 in rng (D1 | j1) ; :: thesis: x1 in rng (D2 | (indx (D2,D1,j1)))

then consider k being Element of NAT such that

A138: k in dom (D1 | j1) and

A139: x1 = (D1 | j1) . k by PARTFUN1:3;

k in Seg (len (D1 | j1)) by A138, FINSEQ_1:def 3;

then A140: k in Seg j1 by A137, FINSEQ_1:59;

then A141: k in dom D1 by A45, RFINSEQ:6;

k <= j1 by A140, FINSEQ_1:1;

then D1 . k <= D1 . j1 by A47, A141, SEQ_4:137;

then D2 . (indx (D2,D1,k)) <= D1 . j1 by A13, A141, INTEGRA1:def 19;

then A142: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by A13, A47, INTEGRA1:def 19;

A143: (D1 | j1) . k = D1 . k by A45, A140, RFINSEQ:6;

D1 . k in rng D1 by A141, FUNCT_1:def 3;

then x1 in rng D2 by A14, A139, A143, XBOOLE_0:def 3;

then consider n being Element of NAT such that

A144: n in dom D2 and

A145: x1 = D2 . n by PARTFUN1:3;

D2 . (indx (D2,D1,k)) = D2 . n by A13, A139, A143, A141, A145, INTEGRA1:def 19;

then A146: n <= indx (D2,D1,j1) by A48, A144, A142, SEQM_3:def 1;

1 <= n by A144, FINSEQ_3:25;

then A147: n in Seg (indx (D2,D1,j1)) by A146, FINSEQ_1:1;

then n in Seg (len (D2 | (indx (D2,D1,j1)))) by A134, FINSEQ_1:59;

then A148: n in dom (D2 | (indx (D2,D1,j1))) by FINSEQ_1:def 3;

D2 . n = (D2 | (indx (D2,D1,j1))) . n by A48, A147, RFINSEQ:6;

hence x1 in rng (D2 | (indx (D2,D1,j1))) by A145, A148, FUNCT_1:def 3; :: thesis: verum

end;assume x1 in rng (D1 | j1) ; :: thesis: x1 in rng (D2 | (indx (D2,D1,j1)))

then consider k being Element of NAT such that

A138: k in dom (D1 | j1) and

A139: x1 = (D1 | j1) . k by PARTFUN1:3;

k in Seg (len (D1 | j1)) by A138, FINSEQ_1:def 3;

then A140: k in Seg j1 by A137, FINSEQ_1:59;

then A141: k in dom D1 by A45, RFINSEQ:6;

k <= j1 by A140, FINSEQ_1:1;

then D1 . k <= D1 . j1 by A47, A141, SEQ_4:137;

then D2 . (indx (D2,D1,k)) <= D1 . j1 by A13, A141, INTEGRA1:def 19;

then A142: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by A13, A47, INTEGRA1:def 19;

A143: (D1 | j1) . k = D1 . k by A45, A140, RFINSEQ:6;

D1 . k in rng D1 by A141, FUNCT_1:def 3;

then x1 in rng D2 by A14, A139, A143, XBOOLE_0:def 3;

then consider n being Element of NAT such that

A144: n in dom D2 and

A145: x1 = D2 . n by PARTFUN1:3;

D2 . (indx (D2,D1,k)) = D2 . n by A13, A139, A143, A141, A145, INTEGRA1:def 19;

then A146: n <= indx (D2,D1,j1) by A48, A144, A142, SEQM_3:def 1;

1 <= n by A144, FINSEQ_3:25;

then A147: n in Seg (indx (D2,D1,j1)) by A146, FINSEQ_1:1;

then n in Seg (len (D2 | (indx (D2,D1,j1)))) by A134, FINSEQ_1:59;

then A148: n in dom (D2 | (indx (D2,D1,j1))) by FINSEQ_1:def 3;

D2 . n = (D2 | (indx (D2,D1,j1))) . n by A48, A147, RFINSEQ:6;

hence x1 in rng (D2 | (indx (D2,D1,j1))) by A145, A148, FUNCT_1:def 3; :: thesis: verum

A150: 1 <= j1 by A136, FINSEQ_1:1;

lower_bound (divset (D1,j)) <= D . 1 by A43, INTEGRA2:1;

then A151: D1 . j1 <= D . 1 by A42, A44, INTEGRA1:def 4;

for x1 being object st x1 in rng (D2 | (indx (D2,D1,j1))) holds

x1 in rng (D1 | j1)

proof

then
rng (D2 | (indx (D2,D1,j1))) c= rng (D1 | j1)
;
let x1 be object ; :: thesis: ( x1 in rng (D2 | (indx (D2,D1,j1))) implies x1 in rng (D1 | j1) )

assume x1 in rng (D2 | (indx (D2,D1,j1))) ; :: thesis: x1 in rng (D1 | j1)

then consider k being Element of NAT such that

A152: k in dom (D2 | (indx (D2,D1,j1))) and

A153: x1 = (D2 | (indx (D2,D1,j1))) . k by PARTFUN1:3;

k in Seg (len (D2 | (indx (D2,D1,j1)))) by A152, FINSEQ_1:def 3;

then A154: k in Seg (indx (D2,D1,j1)) by A134, FINSEQ_1:59;

then A155: k in dom D2 by A48, RFINSEQ:6;

A156: len (D1 | j1) = j1 by A137, FINSEQ_1:59;

k <= indx (D2,D1,j1) by A154, FINSEQ_1:1;

then D2 . k <= D2 . (indx (D2,D1,j1)) by A48, A155, SEQ_4:137;

then A157: D2 . k <= D1 . j1 by A13, A47, INTEGRA1:def 19;

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

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

end;assume x1 in rng (D2 | (indx (D2,D1,j1))) ; :: thesis: x1 in rng (D1 | j1)

then consider k being Element of NAT such that

A152: k in dom (D2 | (indx (D2,D1,j1))) and

A153: x1 = (D2 | (indx (D2,D1,j1))) . k by PARTFUN1:3;

k in Seg (len (D2 | (indx (D2,D1,j1)))) by A152, FINSEQ_1:def 3;

then A154: k in Seg (indx (D2,D1,j1)) by A134, FINSEQ_1:59;

then A155: k in dom D2 by A48, RFINSEQ:6;

A156: len (D1 | j1) = j1 by A137, FINSEQ_1:59;

k <= indx (D2,D1,j1) by A154, FINSEQ_1:1;

then D2 . k <= D2 . (indx (D2,D1,j1)) by A48, A155, SEQ_4:137;

then A157: D2 . k <= D1 . j1 by A13, A47, INTEGRA1:def 19;

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

proof

A164:
( D2 . k in rng D implies D2 . k = D1 . j1 )
assume
D2 . k in rng D1
; :: thesis: D2 . k in rng (D1 | j1)

then consider m being Element of NAT such that

A159: m in dom D1 and

A160: D2 . k = D1 . m by PARTFUN1:3;

m in Seg (len D1) by A159, FINSEQ_1:def 3;

then A161: 1 <= m by FINSEQ_1:1;

A162: m <= j1 by A45, A157, A159, A160, SEQM_3:def 1;

then m in Seg j1 by A161, FINSEQ_1:1;

then A163: D2 . k = (D1 | j1) . m by A45, A160, RFINSEQ:6;

m in dom (D1 | j1) by A156, A161, A162, FINSEQ_3:25;

hence D2 . k in rng (D1 | j1) by A163, FUNCT_1:def 3; :: thesis: verum

end;then consider m being Element of NAT such that

A159: m in dom D1 and

A160: D2 . k = D1 . m by PARTFUN1:3;

m in Seg (len D1) by A159, FINSEQ_1:def 3;

then A161: 1 <= m by FINSEQ_1:1;

A162: m <= j1 by A45, A157, A159, A160, SEQM_3:def 1;

then m in Seg j1 by A161, FINSEQ_1:1;

then A163: D2 . k = (D1 | j1) . m by A45, A160, RFINSEQ:6;

m in dom (D1 | j1) by A156, A161, A162, FINSEQ_3:25;

hence D2 . k in rng (D1 | j1) by A163, FUNCT_1:def 3; :: thesis: verum

proof

A167:
( D2 . k in rng D implies D2 . k in rng (D1 | j1) )
assume
D2 . k in rng D
; :: thesis: D2 . k = D1 . j1

then consider n being Element of NAT such that

A165: n in dom D and

A166: D2 . k = D . n by PARTFUN1:3;

1 <= n by A165, FINSEQ_3:25;

then D . 1 <= D2 . k by A41, A165, A166, SEQ_4:137;

then D1 . j1 <= D2 . k by A151, XXREAL_0:2;

hence D2 . k = D1 . j1 by A157, XXREAL_0:1; :: thesis: verum

end;then consider n being Element of NAT such that

A165: n in dom D and

A166: D2 . k = D . n by PARTFUN1:3;

1 <= n by A165, FINSEQ_3:25;

then D . 1 <= D2 . k by A41, A165, A166, SEQ_4:137;

then D1 . j1 <= D2 . k by A151, XXREAL_0:2;

hence D2 . k = D1 . j1 by A157, XXREAL_0:1; :: thesis: verum

proof

D2 . k in rng D2
by A155, FUNCT_1:def 3;
j1 in Seg (len (D1 | j1))
by A150, A156, FINSEQ_1:1;

then j1 in dom (D1 | j1) by FINSEQ_1:def 3;

then A168: (D1 | j1) . j1 in rng (D1 | j1) by FUNCT_1:def 3;

assume A169: D2 . k in rng D ; :: thesis: D2 . k in rng (D1 | j1)

j1 in Seg j1 by A150, FINSEQ_1:1;

hence D2 . k in rng (D1 | j1) by A45, A164, A169, A168, RFINSEQ:6; :: thesis: verum

end;then j1 in dom (D1 | j1) by FINSEQ_1:def 3;

then A168: (D1 | j1) . j1 in rng (D1 | j1) by FUNCT_1:def 3;

assume A169: D2 . k in rng D ; :: thesis: D2 . k in rng (D1 | j1)

j1 in Seg j1 by A150, FINSEQ_1:1;

hence D2 . k in rng (D1 | j1) by A45, A164, A169, A168, RFINSEQ:6; :: thesis: verum

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

then A170: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A149, XBOOLE_0:def 10;

mid (D1,1,j1) is increasing by A42, A44, A150, INTEGRA1:7, INTEGRA1:35;

then A171: D1 | j1 is increasing by A150, FINSEQ_6:116;

then A172: D2 | (indx (D2,D1,j1)) = D1 | j1 by A51, A170, Th6;

A173: for k being Element of NAT st 1 <= k & k <= j1 holds

k = indx (D2,D1,k)

proof

A191:
for k being Nat st 1 <= k & k <= len ((lower_volume (f,D1)) | j1) holds
let k be Element of NAT ; :: thesis: ( 1 <= k & k <= j1 implies k = indx (D2,D1,k) )

assume that

A174: 1 <= k and

A175: k <= j1 ; :: thesis: k = indx (D2,D1,k)

assume A176: k <> indx (D2,D1,k) ; :: thesis: contradiction

end;assume that

A174: 1 <= k and

A175: k <= j1 ; :: thesis: k = indx (D2,D1,k)

assume A176: k <> indx (D2,D1,k) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k > indx (D2,D1,k) or k < indx (D2,D1,k) )
by A176, XXREAL_0:1;

end;

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

k <= len D1
by A137, A175, XXREAL_0:2;

then A178: k in dom D1 by A174, FINSEQ_3:25;

then indx (D2,D1,k) in dom D2 by A13, INTEGRA1:def 19;

then indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;

then A179: 1 <= indx (D2,D1,k) by FINSEQ_1:1;

A180: indx (D2,D1,k) < j1 by A175, A177, XXREAL_0:2;

then A181: indx (D2,D1,k) in Seg j1 by A179, FINSEQ_1:1;

indx (D2,D1,k) <= indx (D2,D1,j1) by A13, A45, A175, A178, Th7;

then indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A179, FINSEQ_1:1;

then A182: (D2 | (indx (D2,D1,j1))) . (indx (D2,D1,k)) = D2 . (indx (D2,D1,k)) by A48, RFINSEQ:6;

indx (D2,D1,k) <= len D1 by A137, A180, XXREAL_0:2;

then indx (D2,D1,k) in dom D1 by A179, FINSEQ_3:25;

then A183: D1 . k > D1 . (indx (D2,D1,k)) by A177, A178, SEQM_3:def 1;

D1 . k = D2 . (indx (D2,D1,k)) by A13, A178, INTEGRA1:def 19;

hence contradiction by A45, A172, A182, A183, A181, RFINSEQ:6; :: thesis: verum

end;then A178: k in dom D1 by A174, FINSEQ_3:25;

then indx (D2,D1,k) in dom D2 by A13, INTEGRA1:def 19;

then indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;

then A179: 1 <= indx (D2,D1,k) by FINSEQ_1:1;

A180: indx (D2,D1,k) < j1 by A175, A177, XXREAL_0:2;

then A181: indx (D2,D1,k) in Seg j1 by A179, FINSEQ_1:1;

indx (D2,D1,k) <= indx (D2,D1,j1) by A13, A45, A175, A178, Th7;

then indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A179, FINSEQ_1:1;

then A182: (D2 | (indx (D2,D1,j1))) . (indx (D2,D1,k)) = D2 . (indx (D2,D1,k)) by A48, RFINSEQ:6;

indx (D2,D1,k) <= len D1 by A137, A180, XXREAL_0:2;

then indx (D2,D1,k) in dom D1 by A179, FINSEQ_3:25;

then A183: D1 . k > D1 . (indx (D2,D1,k)) by A177, A178, SEQM_3:def 1;

D1 . k = D2 . (indx (D2,D1,k)) by A13, A178, INTEGRA1:def 19;

hence contradiction by A45, A172, A182, A183, A181, RFINSEQ:6; :: thesis: verum

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

k <= len D1
by A137, A175, XXREAL_0:2;

then A185: k in dom D1 by A174, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A13, A45, A175, Th7;

then A186: k <= indx (D2,D1,j1) by A184, XXREAL_0:2;

then k <= len D2 by A134, XXREAL_0:2;

then A187: k in dom D2 by A174, FINSEQ_3:25;

k in Seg j1 by A174, A175, FINSEQ_1:1;

then A188: D1 . k = (D1 | j1) . k by A47, RFINSEQ:6;

indx (D2,D1,k) in dom D2 by A13, A185, INTEGRA1:def 19;

then A189: D2 . k < D2 . (indx (D2,D1,k)) by A184, A187, SEQM_3:def 1;

A190: k in Seg (indx (D2,D1,j1)) by A174, A186, FINSEQ_1:1;

D1 . k = D2 . (indx (D2,D1,k)) by A13, A185, INTEGRA1:def 19;

hence contradiction by A48, A172, A188, A189, A190, RFINSEQ:6; :: thesis: verum

end;then A185: k in dom D1 by A174, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A13, A45, A175, Th7;

then A186: k <= indx (D2,D1,j1) by A184, XXREAL_0:2;

then k <= len D2 by A134, XXREAL_0:2;

then A187: k in dom D2 by A174, FINSEQ_3:25;

k in Seg j1 by A174, A175, FINSEQ_1:1;

then A188: D1 . k = (D1 | j1) . k by A47, RFINSEQ:6;

indx (D2,D1,k) in dom D2 by A13, A185, INTEGRA1:def 19;

then A189: D2 . k < D2 . (indx (D2,D1,k)) by A184, A187, SEQM_3:def 1;

A190: k in Seg (indx (D2,D1,j1)) by A174, A186, FINSEQ_1:1;

D1 . k = D2 . (indx (D2,D1,k)) by A13, A185, INTEGRA1:def 19;

hence contradiction by A48, A172, A188, A189, A190, RFINSEQ:6; :: thesis: verum

((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k

proof

indx (D2,D1,j1) in dom D2
by A13, A47, INTEGRA1:def 19;
indx (D2,D1,j1) in Seg (len D2)
by A48, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len (lower_volume (f,D2))) by INTEGRA1:def 7;

then A192: indx (D2,D1,j1) in dom (lower_volume (f,D2)) by FINSEQ_1:def 3;

let k be Nat; :: thesis: ( 1 <= k & k <= len ((lower_volume (f,D1)) | j1) implies ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k )

assume that

A193: 1 <= k and

A194: k <= len ((lower_volume (f,D1)) | j1) ; :: thesis: ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A195: len (lower_volume (f,D1)) = len D1 by INTEGRA1:def 7;

then A196: k <= j1 by A137, A194, FINSEQ_1:59;

then k <= len D1 by A137, XXREAL_0:2;

then A197: k in Seg (len D1) by A193, FINSEQ_1:1;

then A198: k in dom D1 by FINSEQ_1:def 3;

then A199: indx (D2,D1,k) in dom D2 by A13, INTEGRA1:def 19;

A200: k in Seg j1 by A193, A196, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A173, A193, A196;

then A201: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A150, A173;

then indx (D2,D1,k) <= indx (D2,D1,j1) by FINSEQ_1:1;

then A202: indx (D2,D1,k) <= len D2 by A134, XXREAL_0:2;

A203: D1 . k = D2 . (indx (D2,D1,k)) by A13, A198, INTEGRA1:def 19;

A204: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

then A216: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A204, INTEGRA1:4;

A217: k in dom D1 by A197, FINSEQ_1:def 3;

j1 in Seg (len (lower_volume (f,D1))) by A45, A195, FINSEQ_1:def 3;

then j1 in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;

then A218: ((lower_volume (f,D1)) | j1) . k = (lower_volume (f,D1)) . k by A200, RFINSEQ:6

.= (lower_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A217, A216, INTEGRA1:def 7 ;

1 <= indx (D2,D1,k) by A173, A193, A196;

then indx (D2,D1,k) in Seg (len D2) by A202, FINSEQ_1:1;

then A219: indx (D2,D1,k) in dom D2 by FINSEQ_1:def 3;

((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A173, A193, A196

.= (lower_volume (f,D2)) . (indx (D2,D1,k)) by A201, A192, RFINSEQ:6

.= (lower_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A219, INTEGRA1:def 7 ;

hence ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k by A218; :: thesis: verum

end;then indx (D2,D1,j1) in Seg (len (lower_volume (f,D2))) by INTEGRA1:def 7;

then A192: indx (D2,D1,j1) in dom (lower_volume (f,D2)) by FINSEQ_1:def 3;

let k be Nat; :: thesis: ( 1 <= k & k <= len ((lower_volume (f,D1)) | j1) implies ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k )

assume that

A193: 1 <= k and

A194: k <= len ((lower_volume (f,D1)) | j1) ; :: thesis: ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A195: len (lower_volume (f,D1)) = len D1 by INTEGRA1:def 7;

then A196: k <= j1 by A137, A194, FINSEQ_1:59;

then k <= len D1 by A137, XXREAL_0:2;

then A197: k in Seg (len D1) by A193, FINSEQ_1:1;

then A198: k in dom D1 by FINSEQ_1:def 3;

then A199: indx (D2,D1,k) in dom D2 by A13, INTEGRA1:def 19;

A200: k in Seg j1 by A193, A196, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A173, A193, A196;

then A201: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A150, A173;

then indx (D2,D1,k) <= indx (D2,D1,j1) by FINSEQ_1:1;

then A202: indx (D2,D1,k) <= len D2 by A134, XXREAL_0:2;

A203: D1 . k = D2 . (indx (D2,D1,k)) by A13, A198, INTEGRA1:def 19;

A204: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

proof
end;

divset (D2,(indx (D2,D1,k))) = [.(lower_bound (divset (D2,(indx (D2,D1,k))))),(upper_bound (divset (D2,(indx (D2,D1,k))))).]
by INTEGRA1:4;per cases
( k = 1 or k <> 1 )
;

end;

suppose A205:
k = 1
; :: thesis: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

then A206:
upper_bound (divset (D1,k)) = D1 . k
by A198, INTEGRA1:def 4;

A207: lower_bound (divset (D1,k)) = lower_bound A by A198, A205, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A150, A173, A205;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A199, A203, A207, A206, INTEGRA1:def 4; :: thesis: verum

end;A207: lower_bound (divset (D1,k)) = lower_bound A by A198, A205, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A150, A173, A205;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A199, A203, A207, A206, INTEGRA1:def 4; :: thesis: verum

suppose A208:
k <> 1
; :: thesis: ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) )

then reconsider k1 = k - 1 as Element of NAT by A198, INTEGRA1:7;

k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A209: k1 <= j1 by A196, XXREAL_0:2;

A210: k - 1 in dom D1 by A198, A208, INTEGRA1:7;

then k1 in Seg (len D1) by FINSEQ_1:def 3;

then 1 <= k1 by FINSEQ_1:1;

then k1 = indx (D2,D1,k1) by A173, A209;

then A211: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A173, A193, A196;

A212: indx (D2,D1,k) <> 1 by A173, A193, A196, A208;

then A213: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A199, INTEGRA1:def 4;

A214: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A199, A212, INTEGRA1:def 4;

A215: upper_bound (divset (D1,k)) = D1 . k by A198, A208, INTEGRA1:def 4;

lower_bound (divset (D1,k)) = D1 . (k - 1) by A198, A208, INTEGRA1:def 4;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A13, A198, A215, A210, A213, A214, A211, INTEGRA1:def 19; :: thesis: verum

end;k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A209: k1 <= j1 by A196, XXREAL_0:2;

A210: k - 1 in dom D1 by A198, A208, INTEGRA1:7;

then k1 in Seg (len D1) by FINSEQ_1:def 3;

then 1 <= k1 by FINSEQ_1:1;

then k1 = indx (D2,D1,k1) by A173, A209;

then A211: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A173, A193, A196;

A212: indx (D2,D1,k) <> 1 by A173, A193, A196, A208;

then A213: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A199, INTEGRA1:def 4;

A214: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A199, A212, INTEGRA1:def 4;

A215: upper_bound (divset (D1,k)) = D1 . k by A198, A208, INTEGRA1:def 4;

lower_bound (divset (D1,k)) = D1 . (k - 1) by A198, A208, INTEGRA1:def 4;

hence ( lower_bound (divset (D1,k)) = lower_bound (divset (D2,(indx (D2,D1,k)))) & upper_bound (divset (D1,k)) = upper_bound (divset (D2,(indx (D2,D1,k)))) ) by A13, A198, A215, A210, A213, A214, A211, INTEGRA1:def 19; :: thesis: verum

then A216: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A204, INTEGRA1:4;

A217: k in dom D1 by A197, FINSEQ_1:def 3;

j1 in Seg (len (lower_volume (f,D1))) by A45, A195, FINSEQ_1:def 3;

then j1 in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;

then A218: ((lower_volume (f,D1)) | j1) . k = (lower_volume (f,D1)) . k by A200, RFINSEQ:6

.= (lower_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A217, A216, INTEGRA1:def 7 ;

1 <= indx (D2,D1,k) by A173, A193, A196;

then indx (D2,D1,k) in Seg (len D2) by A202, FINSEQ_1:1;

then A219: indx (D2,D1,k) in dom D2 by FINSEQ_1:def 3;

((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A173, A193, A196

.= (lower_volume (f,D2)) . (indx (D2,D1,k)) by A201, A192, RFINSEQ:6

.= (lower_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A219, INTEGRA1:def 7 ;

hence ((lower_volume (f,D1)) | j1) . k = ((lower_volume (f,D2)) | (indx (D2,D1,j1))) . k by A218; :: thesis: verum

then indx (D2,D1,j1) <= len D2 by FINSEQ_3:25;

then A220: indx (D2,D1,j1) <= len (lower_volume (f,D2)) by INTEGRA1:def 7;

j1 <= len D1 by A47, FINSEQ_3:25;

then A221: j1 <= len (lower_volume (f,D1)) by INTEGRA1:def 7;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A51, A171, A170, Th6;

then indx (D2,D1,j1) = j1 by A137, A135, FINSEQ_1:59;

then len ((lower_volume (f,D1)) | j1) = indx (D2,D1,j1) by A221, FINSEQ_1:59;

then len ((lower_volume (f,D1)) | j1) = len ((lower_volume (f,D2)) | (indx (D2,D1,j1))) by A220, FINSEQ_1:59;

then A222: (lower_volume (f,D2)) | (indx (D2,D1,j1)) = (lower_volume (f,D1)) | j1 by A191, FINSEQ_1:14;

A223: j in Seg (len D1) by A42, FINSEQ_1:def 3;

then A224: 1 <= j by FINSEQ_1:1;

indx (D2,D1,j) in Seg (len H

then A225: indx (D2,D1,j) in dom H

indx (D2,D1,j) <= len D2 by A132, FINSEQ_1:1;

then A226: indx (D2,D1,j) <= len H

j in Seg (len H

then A227: j in dom H

j <= len D1 by A223, FINSEQ_1:1;

then A228: j <= len H

j1 in Seg (len D1) by A45, FINSEQ_1:def 3;

then j1 in Seg (len H

then j1 in dom H

then H

then H

.= Sum ((mid (H

.= Sum (mid (H

.= Sum (H

then A229: H

indx (D2,D1,j1) in Seg (len D2) by A48, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len H

then indx (D2,D1,j1) in dom H

then H

then H

.= Sum ((mid (H

.= Sum (mid (H

.= Sum (H

then A230: H

indx (D2,D1,j1) in Seg (len D2) by A48, FINSEQ_1:def 3;

then indx (D2,D1,j1) in Seg (len (lower_volume (f,D2))) by INTEGRA1:def 7;

then indx (D2,D1,j1) in dom (lower_volume (f,D2)) by FINSEQ_1:def 3;

then H

.= H

hence H

A231: for i being non zero Nat st S

S

proof

let i be non zero Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

A232: i >= 1 by NAT_1:14;

assume A233: S_{1}[i]
; :: thesis: S_{1}[i + 1]

S_{1}[i + 1]

A232: i >= 1 by NAT_1:14;

assume A233: S

S

proof

A234:
i <= i + 1
by NAT_1:11;

assume A235: i + 1 in dom D ; :: thesis: ex j being Element of NAT st

( j in dom D1 & D . (i + 1) in divset (D1,j) & H_{2}(D2, indx (D2,D1,j)) - H_{2}(D1,j) <= ((i + 1) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

then consider j being Element of NAT such that

A236: j in dom D1 and

A237: D . (i + 1) in divset (D1,j) by Th3, INTEGRA1:6;

A238: D2 . (indx (D2,D1,j)) = D1 . j by A13, A236, INTEGRA1:def 19;

i + 1 <= len D by A235, FINSEQ_3:25;

then i <= len D by A234, XXREAL_0:2;

then A239: i in Seg (len D) by A232, FINSEQ_1:1;

then A240: i in dom D by FINSEQ_1:def 3;

consider n1 being Element of NAT such that

A241: n1 in dom D1 and

A242: D . i in divset (D1,n1) and

A243: H_{2}(D2, indx (D2,D1,n1)) - H_{2}(D1,n1) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)
by A233, A239, FINSEQ_1:def 3;

A244: 1 <= n1 + 1 by NAT_1:12;

A245: n1 < j

A258: 1 <= n1 by A241, FINSEQ_3:25;

A259: indx (D2,D1,n1) in dom D2 by A13, A241, INTEGRA1:def 19;

then A260: 1 <= indx (D2,D1,n1) by FINSEQ_3:25;

A261: indx (D2,D1,j) in dom D2 by A13, A236, INTEGRA1:def 19;

then A262: 1 <= indx (D2,D1,j) by FINSEQ_3:25;

A263: indx (D2,D1,j) <= len D2 by A261, FINSEQ_3:25;

then A264: indx (D2,D1,j) <= len H_{1}(D2)
by INTEGRA1:def 7;

A265: 1 <= j by A236, FINSEQ_3:25;

A266: j <= len D1 by A236, FINSEQ_3:25;

then A267: n1 + 1 <= len D1 by A257, XXREAL_0:2;

then A268: n1 + 1 in dom D1 by A244, FINSEQ_3:25;

then A269: indx (D2,D1,(n1 + 1)) in dom D2 by A13, INTEGRA1:def 19;

then A270: 1 <= indx (D2,D1,(n1 + 1)) by FINSEQ_3:25;

A271: D2 . (indx (D2,D1,(n1 + 1))) = D1 . (n1 + 1) by A13, A268, INTEGRA1:def 19;

then D2 . (indx (D2,D1,(n1 + 1))) <= D2 . (indx (D2,D1,j)) by A236, A257, A268, A238, SEQ_4:137;

then A272: indx (D2,D1,(n1 + 1)) <= indx (D2,D1,j) by A269, A261, SEQM_3:def 1;

then 1 + (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) + 1 by XREAL_1:6;

then 1 <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;

then A273: (mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j)))) . 1 = D2 . ((1 - 1) + (indx (D2,D1,(n1 + 1)))) by A272, A270, A263, FINSEQ_6:122

.= D1 . (n1 + 1) by A13, A268, INTEGRA1:def 19 ;

A274: D2 . (indx (D2,D1,n1)) = D1 . n1 by A13, A241, INTEGRA1:def 19;

A275: j <= len H_{1}(D1)
by A266, INTEGRA1:def 7;

then j in Seg (len H_{1}(D1))
by A265, FINSEQ_1:1;

then A276: j in dom H_{1}(D1)
by FINSEQ_1:def 3;

A277: indx (D2,D1,(n1 + 1)) <= len D2 by A269, FINSEQ_3:25;

n1 in Seg (len D1) by A241, FINSEQ_1:def 3;

then n1 in Seg (len H_{1}(D1))
by INTEGRA1:def 7;

then n1 in dom H_{1}(D1)
by FINSEQ_1:def 3;

then H_{2}(D1,n1) =
Sum (H_{1}(D1) | n1)
by INTEGRA1:def 20

.= Sum (mid (H_{1}(D1),1,n1))
by A258, FINSEQ_6:116
;

then H_{2}(D1,n1) + (Sum (mid (H_{1}(D1),(n1 + 1),j))) =
Sum ((mid (H_{1}(D1),1,n1)) ^ (mid (H_{1}(D1),(n1 + 1),j)))
by RVSUM_1:75

.= Sum (mid (H_{1}(D1),1,j))
by A245, A258, A275, INTEGRA2:4

.= Sum (H_{1}(D1) | j)
by A265, FINSEQ_6:116
;

then A278: H_{2}(D1,j) = H_{2}(D1,n1) + (Sum (mid (H_{1}(D1),(n1 + 1),j)))
by A276, INTEGRA1:def 20;

indx (D2,D1,j) in Seg (len D2) by A261, FINSEQ_1:def 3;

then indx (D2,D1,j) in Seg (len H_{1}(D2))
by INTEGRA1:def 7;

then A279: indx (D2,D1,j) in dom H_{1}(D2)
by FINSEQ_1:def 3;

A280: n1 >= 1 by A241, FINSEQ_3:25;

A281: j - n1 >= 1 by A257, XREAL_1:19;

(Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

assume A235: i + 1 in dom D ; :: thesis: ex j being Element of NAT st

( j in dom D1 & D . (i + 1) in divset (D1,j) & H

then consider j being Element of NAT such that

A236: j in dom D1 and

A237: D . (i + 1) in divset (D1,j) by Th3, INTEGRA1:6;

A238: D2 . (indx (D2,D1,j)) = D1 . j by A13, A236, INTEGRA1:def 19;

i + 1 <= len D by A235, FINSEQ_3:25;

then i <= len D by A234, XXREAL_0:2;

then A239: i in Seg (len D) by A232, FINSEQ_1:1;

then A240: i in dom D by FINSEQ_1:def 3;

consider n1 being Element of NAT such that

A241: n1 in dom D1 and

A242: D . i in divset (D1,n1) and

A243: H

A244: 1 <= n1 + 1 by NAT_1:12;

A245: n1 < j

proof

then A257:
n1 + 1 <= j
by NAT_1:13;
assume A246:
n1 >= j
; :: thesis: contradiction

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( n1 = j or n1 > j )
by A246, XXREAL_0:1;

end;

suppose A247:
n1 = j
; :: thesis: contradiction

D . i in rng D
by A240, FUNCT_1:def 3;

then A248: D . i in (rng D) /\ (divset (D1,j)) by A242, A247, XBOOLE_0:def 4;

D . (i + 1) in rng D by A235, FUNCT_1:def 3;

then A249: D . (i + 1) in (rng D) /\ (divset (D1,j)) by A237, XBOOLE_0:def 4;

i + 1 > i by XREAL_1:29;

hence contradiction by A11, A235, A236, A240, A248, A249, Th5, SEQ_4:138; :: thesis: verum

end;then A248: D . i in (rng D) /\ (divset (D1,j)) by A242, A247, XBOOLE_0:def 4;

D . (i + 1) in rng D by A235, FUNCT_1:def 3;

then A249: D . (i + 1) in (rng D) /\ (divset (D1,j)) by A237, XBOOLE_0:def 4;

i + 1 > i by XREAL_1:29;

hence contradiction by A11, A235, A236, A240, A248, A249, Th5, SEQ_4:138; :: thesis: verum

suppose
n1 > j
; :: thesis: contradiction

then A250:
n1 >= j + 1
by NAT_1:13;

then A251: n1 - 1 >= j by XREAL_1:19;

1 <= j by A236, FINSEQ_3:25;

then 1 + 1 <= j + 1 by XREAL_1:6;

then A252: n1 <> 1 by A250, XXREAL_0:2;

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

then A253: D . i >= D1 . (n1 - 1) by A241, A252, INTEGRA1:def 4;

n1 - 1 in dom D1 by A241, A252, INTEGRA1:7;

then D1 . j <= D1 . (n1 - 1) by A236, A251, SEQ_4:137;

then A254: D . i >= D1 . j by A253, XXREAL_0:2;

A255: i < i + 1 by XREAL_1:29;

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

then D . i >= D . (i + 1) by A256, A254, XXREAL_0:2;

hence contradiction by A235, A240, A255, SEQM_3:def 1; :: thesis: verum

end;then A251: n1 - 1 >= j by XREAL_1:19;

1 <= j by A236, FINSEQ_3:25;

then 1 + 1 <= j + 1 by XREAL_1:6;

then A252: n1 <> 1 by A250, XXREAL_0:2;

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

then A253: D . i >= D1 . (n1 - 1) by A241, A252, INTEGRA1:def 4;

n1 - 1 in dom D1 by A241, A252, INTEGRA1:7;

then D1 . j <= D1 . (n1 - 1) by A236, A251, SEQ_4:137;

then A254: D . i >= D1 . j by A253, XXREAL_0:2;

A255: i < i + 1 by XREAL_1:29;

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

proof
end;

D . (i + 1) <= upper_bound (divset (D1,j))
by A237, INTEGRA2:1;then D . i >= D . (i + 1) by A256, A254, XXREAL_0:2;

hence contradiction by A235, A240, A255, SEQM_3:def 1; :: thesis: verum

A258: 1 <= n1 by A241, FINSEQ_3:25;

A259: indx (D2,D1,n1) in dom D2 by A13, A241, INTEGRA1:def 19;

then A260: 1 <= indx (D2,D1,n1) by FINSEQ_3:25;

A261: indx (D2,D1,j) in dom D2 by A13, A236, INTEGRA1:def 19;

then A262: 1 <= indx (D2,D1,j) by FINSEQ_3:25;

A263: indx (D2,D1,j) <= len D2 by A261, FINSEQ_3:25;

then A264: indx (D2,D1,j) <= len H

A265: 1 <= j by A236, FINSEQ_3:25;

A266: j <= len D1 by A236, FINSEQ_3:25;

then A267: n1 + 1 <= len D1 by A257, XXREAL_0:2;

then A268: n1 + 1 in dom D1 by A244, FINSEQ_3:25;

then A269: indx (D2,D1,(n1 + 1)) in dom D2 by A13, INTEGRA1:def 19;

then A270: 1 <= indx (D2,D1,(n1 + 1)) by FINSEQ_3:25;

A271: D2 . (indx (D2,D1,(n1 + 1))) = D1 . (n1 + 1) by A13, A268, INTEGRA1:def 19;

then D2 . (indx (D2,D1,(n1 + 1))) <= D2 . (indx (D2,D1,j)) by A236, A257, A268, A238, SEQ_4:137;

then A272: indx (D2,D1,(n1 + 1)) <= indx (D2,D1,j) by A269, A261, SEQM_3:def 1;

then 1 + (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) + 1 by XREAL_1:6;

then 1 <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;

then A273: (mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j)))) . 1 = D2 . ((1 - 1) + (indx (D2,D1,(n1 + 1)))) by A272, A270, A263, FINSEQ_6:122

.= D1 . (n1 + 1) by A13, A268, INTEGRA1:def 19 ;

A274: D2 . (indx (D2,D1,n1)) = D1 . n1 by A13, A241, INTEGRA1:def 19;

A275: j <= len H

then j in Seg (len H

then A276: j in dom H

A277: indx (D2,D1,(n1 + 1)) <= len D2 by A269, FINSEQ_3:25;

n1 in Seg (len D1) by A241, FINSEQ_1:def 3;

then n1 in Seg (len H

then n1 in dom H

then H

.= Sum (mid (H

then H

.= Sum (mid (H

.= Sum (H

then A278: H

indx (D2,D1,j) in Seg (len D2) by A261, FINSEQ_1:def 3;

then indx (D2,D1,j) in Seg (len H

then A279: indx (D2,D1,j) in dom H

A280: n1 >= 1 by A241, FINSEQ_3:25;

A281: j - n1 >= 1 by A257, XREAL_1:19;

(Sum (mid (H

proof

now :: thesis: (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

per cases
( n1 + 1 = j or n1 + 1 < j )
by A257, XXREAL_0:1;

suppose A282:
n1 + 1 = j
; :: thesis: (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

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

A313: indx (D2,D1,j) <= len H_{1}(D2)
by A263, INTEGRA1:def 7;

D1 . n1 < D1 . j by A236, A241, A245, SEQM_3:def 1;

then A314: indx (D2,D1,n1) < indx (D2,D1,j) by A259, A274, A261, A238, SEQ_4:137;

then A315: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by NAT_1:13;

then (indx (D2,D1,n1)) + 1 <= len D2 by A263, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len H_{1}(D2)
by INTEGRA1:def 7;

then A316: len (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) =
((indx (D2,D1,j)) -' ((indx (D2,D1,n1)) + 1)) + 1
by A262, A315, A312, A313, FINSEQ_6:118

.= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A315, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,n1)) ;

(indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A314, NAT_1:13;

then A317: ( (indx (D2,D1,n1)) + 1 = indx (D2,D1,j) or (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ) by XXREAL_0:1;

A318: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
_{1}(D1)
by A267, INTEGRA1:def 7;

then A345: len (mid (H_{1}(D1),(n1 + 1),j)) =
(j -' (n1 + 1)) + 1
by A244, A282, FINSEQ_6:118

.= (j - j) + 1 by A282, XREAL_1:233

.= 1 ;

reconsider lv = (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) as Element of REAL by XREAL_0:def 1;

(n1 + 1) + 1 <= j + 1 by A257, XREAL_1:6;

then 1 <= (j + 1) - (n1 + 1) by XREAL_1:19;

then (mid (H_{1}(D1),(n1 + 1),j)) . 1 =
H_{1}(D1) . ((1 - 1) + (n1 + 1))
by A244, A282, A344, FINSEQ_6:122

.= (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) by A268, INTEGRA1:def 7 ;

then mid (H_{1}(D1),(n1 + 1),j) = <*lv*>
by A345, FINSEQ_1:40;

then A346: Sum (mid (H_{1}(D1),(n1 + 1),j)) = (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1))))
by FINSOP_1:11;

divset (D1,(n1 + 1)) c= A by A268, INTEGRA1:8;

then A347: lower_bound (rng (f | (divset (D1,(n1 + 1))))) >= lower_bound (rng f) by A1, Lm4;

n1 + 1 in Seg (len D1) by A268, FINSEQ_1:def 3;

then n1 + 1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;

then A348: n1 + 1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;

vol (divset (D1,(n1 + 1))) = (upper_volume ((chi (A,A)),D1)) . (n1 + 1) by A268, INTEGRA1:20;

then vol (divset (D1,(n1 + 1))) in rng (upper_volume ((chi (A,A)),D1)) by A348, FUNCT_1:def 3;

then A349: vol (divset (D1,(n1 + 1))) <= delta D1 by XXREAL_2:def 8;

(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;

then A350: ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,(n1 + 1)))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A349, XREAL_1:64;

vol (divset (D1,(n1 + 1))) >= 0 by INTEGRA1:9;

then Sum (mid (H_{1}(D1),(n1 + 1),j)) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A346, A347, XREAL_1:64;

then (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))) - ((lower_bound (rng f)) * (vol (divset (D1,(n1 + 1)))))
by A318, XREAL_1:13;

hence (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
by A350, XXREAL_0:2; :: thesis: verum

end;proof

A310:
( (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) implies (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) )
A284:
upper_bound (divset (D1,j)) = D1 . j
by A236, A245, A280, INTEGRA1:def 4;

A285: lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

A286: 1 <= (indx (D2,D1,n1)) + 1 by A260, NAT_1:13;

assume (indx (D2,D1,j)) - (indx (D2,D1,n1)) > 2 ; :: thesis: contradiction

then A287: (indx (D2,D1,n1)) + 2 < indx (D2,D1,j) by XREAL_1:20;

then A288: (indx (D2,D1,n1)) + 2 <= len D2 by A263, XXREAL_0:2;

A289: (indx (D2,D1,n1)) + 1 < (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then A290: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 2 by NAT_1:13;

then 1 <= (indx (D2,D1,n1)) + 2 by A260, XXREAL_0:2;

then A291: (indx (D2,D1,n1)) + 2 in dom D2 by A288, FINSEQ_3:25;

then A292: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 2) by A261, A287, SEQ_4:137;

A293: not D2 . ((indx (D2,D1,n1)) + 2) in rng D1

then A297: D2 . ((indx (D2,D1,n1)) + 2) in rng D by A14, A293, XBOOLE_0:def 3;

A298: lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

A299: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;

D2 . ((indx (D2,D1,n1)) + 2) >= D2 . (indx (D2,D1,n1)) by A259, A290, A291, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 2) in divset (D1,j) by A274, A238, A282, A298, A284, A292, INTEGRA2:1;

then A300: D2 . ((indx (D2,D1,n1)) + 2) in (rng D) /\ (divset (D1,j)) by A297, XBOOLE_0:def 4;

A301: (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) by A287, A289, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len D2 by A263, XXREAL_0:2;

then A302: (indx (D2,D1,n1)) + 1 in dom D2 by A286, FINSEQ_3:25;

then A303: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 1) by A261, A301, SEQ_4:137;

A304: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A305: not D2 . ((indx (D2,D1,n1)) + 1) in rng D1

then A309: D2 . ((indx (D2,D1,n1)) + 1) in rng D by A14, A305, XBOOLE_0:def 3;

D2 . ((indx (D2,D1,n1)) + 1) >= D2 . (indx (D2,D1,n1)) by A259, A304, A302, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 1) in divset (D1,j) by A274, A238, A282, A285, A299, A303, INTEGRA2:1;

then D2 . ((indx (D2,D1,n1)) + 1) in (rng D) /\ (divset (D1,j)) by A309, XBOOLE_0:def 4;

then D2 . ((indx (D2,D1,n1)) + 1) = D2 . ((indx (D2,D1,n1)) + 2) by A11, A236, A300, Th5;

hence contradiction by A289, A302, A291, SEQM_3:def 1; :: thesis: verum

end;A285: lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

A286: 1 <= (indx (D2,D1,n1)) + 1 by A260, NAT_1:13;

assume (indx (D2,D1,j)) - (indx (D2,D1,n1)) > 2 ; :: thesis: contradiction

then A287: (indx (D2,D1,n1)) + 2 < indx (D2,D1,j) by XREAL_1:20;

then A288: (indx (D2,D1,n1)) + 2 <= len D2 by A263, XXREAL_0:2;

A289: (indx (D2,D1,n1)) + 1 < (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then A290: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 2 by NAT_1:13;

then 1 <= (indx (D2,D1,n1)) + 2 by A260, XXREAL_0:2;

then A291: (indx (D2,D1,n1)) + 2 in dom D2 by A288, FINSEQ_3:25;

then A292: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 2) by A261, A287, SEQ_4:137;

A293: not D2 . ((indx (D2,D1,n1)) + 2) in rng D1

proof

D2 . ((indx (D2,D1,n1)) + 2) in rng D2
by A291, FUNCT_1:def 3;
assume
D2 . ((indx (D2,D1,n1)) + 2) in rng D1
; :: thesis: contradiction

then consider k1 being Element of NAT such that

A294: k1 in dom D1 and

A295: D2 . ((indx (D2,D1,n1)) + 2) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 2) < D2 . (indx (D2,D1,j)) by A261, A287, A291, SEQM_3:def 1;

then A296: k1 < j by A236, A238, A294, A295, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 2) by A259, A290, A291, SEQM_3:def 1;

then n1 < k1 by A241, A274, A294, A295, SEQ_4:137;

hence contradiction by A282, A296, NAT_1:13; :: thesis: verum

end;then consider k1 being Element of NAT such that

A294: k1 in dom D1 and

A295: D2 . ((indx (D2,D1,n1)) + 2) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 2) < D2 . (indx (D2,D1,j)) by A261, A287, A291, SEQM_3:def 1;

then A296: k1 < j by A236, A238, A294, A295, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 2) by A259, A290, A291, SEQM_3:def 1;

then n1 < k1 by A241, A274, A294, A295, SEQ_4:137;

hence contradiction by A282, A296, NAT_1:13; :: thesis: verum

then A297: D2 . ((indx (D2,D1,n1)) + 2) in rng D by A14, A293, XBOOLE_0:def 3;

A298: lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

A299: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;

D2 . ((indx (D2,D1,n1)) + 2) >= D2 . (indx (D2,D1,n1)) by A259, A290, A291, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 2) in divset (D1,j) by A274, A238, A282, A298, A284, A292, INTEGRA2:1;

then A300: D2 . ((indx (D2,D1,n1)) + 2) in (rng D) /\ (divset (D1,j)) by A297, XBOOLE_0:def 4;

A301: (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) by A287, A289, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len D2 by A263, XXREAL_0:2;

then A302: (indx (D2,D1,n1)) + 1 in dom D2 by A286, FINSEQ_3:25;

then A303: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 1) by A261, A301, SEQ_4:137;

A304: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A305: not D2 . ((indx (D2,D1,n1)) + 1) in rng D1

proof

D2 . ((indx (D2,D1,n1)) + 1) in rng D2
by A302, FUNCT_1:def 3;
assume
D2 . ((indx (D2,D1,n1)) + 1) in rng D1
; :: thesis: contradiction

then consider k1 being Element of NAT such that

A306: k1 in dom D1 and

A307: D2 . ((indx (D2,D1,n1)) + 1) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 1) < D2 . (indx (D2,D1,j)) by A261, A301, A302, SEQM_3:def 1;

then A308: k1 < j by A236, A238, A306, A307, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A259, A304, A302, SEQM_3:def 1;

then n1 < k1 by A241, A274, A306, A307, SEQ_4:137;

hence contradiction by A282, A308, NAT_1:13; :: thesis: verum

end;then consider k1 being Element of NAT such that

A306: k1 in dom D1 and

A307: D2 . ((indx (D2,D1,n1)) + 1) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 1) < D2 . (indx (D2,D1,j)) by A261, A301, A302, SEQM_3:def 1;

then A308: k1 < j by A236, A238, A306, A307, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A259, A304, A302, SEQM_3:def 1;

then n1 < k1 by A241, A274, A306, A307, SEQ_4:137;

hence contradiction by A282, A308, NAT_1:13; :: thesis: verum

then A309: D2 . ((indx (D2,D1,n1)) + 1) in rng D by A14, A305, XBOOLE_0:def 3;

D2 . ((indx (D2,D1,n1)) + 1) >= D2 . (indx (D2,D1,n1)) by A259, A304, A302, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 1) in divset (D1,j) by A274, A238, A282, A285, A299, A303, INTEGRA2:1;

then D2 . ((indx (D2,D1,n1)) + 1) in (rng D) /\ (divset (D1,j)) by A309, XBOOLE_0:def 4;

then D2 . ((indx (D2,D1,n1)) + 1) = D2 . ((indx (D2,D1,n1)) + 2) by A11, A236, A300, Th5;

hence contradiction by A289, A302, A291, SEQM_3:def 1; :: thesis: verum

proof

A312:
1 <= (indx (D2,D1,n1)) + 1
by NAT_1:12;
assume
(indx (D2,D1,n1)) + 1 < indx (D2,D1,j)
; :: thesis: (indx (D2,D1,n1)) + 2 = indx (D2,D1,j)

then A311: ((indx (D2,D1,n1)) + 1) + 1 <= indx (D2,D1,j) by NAT_1:13;

(indx (D2,D1,n1)) + 2 >= indx (D2,D1,j) by A283, XREAL_1:20;

hence (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) by A311, XXREAL_0:1; :: thesis: verum

end;then A311: ((indx (D2,D1,n1)) + 1) + 1 <= indx (D2,D1,j) by NAT_1:13;

(indx (D2,D1,n1)) + 2 >= indx (D2,D1,j) by A283, XREAL_1:20;

hence (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) by A311, XXREAL_0:1; :: thesis: verum

A313: indx (D2,D1,j) <= len H

D1 . n1 < D1 . j by A236, A241, A245, SEQM_3:def 1;

then A314: indx (D2,D1,n1) < indx (D2,D1,j) by A259, A274, A261, A238, SEQ_4:137;

then A315: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by NAT_1:13;

then (indx (D2,D1,n1)) + 1 <= len D2 by A263, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len H

then A316: len (mid (H

.= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A315, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,n1)) ;

(indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A314, NAT_1:13;

then A317: ( (indx (D2,D1,n1)) + 1 = indx (D2,D1,j) or (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ) by XXREAL_0:1;

A318: Sum (mid (H

proof
end;

A344:
n1 + 1 <= len Hper cases
( (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1 or (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2 )
by A317, A310;

end;

suppose A319:
(indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1
; :: thesis: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))

A320:
(indx (D2,D1,n1)) + 1 > 1
by A260, NAT_1:13;

then upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A261, A319, INTEGRA1:def 4;

then A321: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . j by A13, A236, A319, INTEGRA1:def 19;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A261, A319, A320, INTEGRA1:def 4;

then A322: lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . n1 by A13, A241, INTEGRA1:def 19;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A280, A268, A282, INTEGRA1:def 4;

then A323: divset (D2,((indx (D2,D1,n1)) + 1)) = divset (D1,(n1 + 1)) by A245, A280, A268, A282, A322, A321, INTEGRA1:def 4;

A324: vol (divset (D2,((indx (D2,D1,n1)) + 1))) >= 0 by INTEGRA1:9;

reconsider LV = H_{1}(D2) . ((indx (D2,D1,n1)) + 1) as Element of REAL by XREAL_0:def 1;

1 = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A319;

then (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 1 =
H_{1}(D2) . ((1 + ((indx (D2,D1,n1)) + 1)) - 1)
by A312, A313, FINSEQ_6:122

.= H_{1}(D2) . ((indx (D2,D1,n1)) + 1)
;

then A325: mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*LV*>
by A316, A319, FINSEQ_1:40;

H_{1}(D2) . ((indx (D2,D1,n1)) + 1) = (lower_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))
by A261, A319, INTEGRA1:def 7;

then H_{1}(D2) . ((indx (D2,D1,n1)) + 1) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A1, A261, A319, A323, A324, Th18, XREAL_1:64;

hence Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A325, FINSOP_1:11; :: thesis: verum

end;then upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A261, A319, INTEGRA1:def 4;

then A321: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . j by A13, A236, A319, INTEGRA1:def 19;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A261, A319, A320, INTEGRA1:def 4;

then A322: lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . n1 by A13, A241, INTEGRA1:def 19;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A280, A268, A282, INTEGRA1:def 4;

then A323: divset (D2,((indx (D2,D1,n1)) + 1)) = divset (D1,(n1 + 1)) by A245, A280, A268, A282, A322, A321, INTEGRA1:def 4;

A324: vol (divset (D2,((indx (D2,D1,n1)) + 1))) >= 0 by INTEGRA1:9;

reconsider LV = H

1 = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A319;

then (mid (H

.= H

then A325: mid (H

H

then H

hence Sum (mid (H

suppose A326:
(indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2
; :: thesis: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))

(indx (D2,D1,n1)) + 2 >= 2 + 1
by A260, XREAL_1:6;

then A327: (indx (D2,D1,n1)) + 2 <> 1 ;

then A328: upper_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . (indx (D2,D1,j)) by A261, A326, INTEGRA1:def 4;

((indx (D2,D1,n1)) + 2) - 1 = (indx (D2,D1,n1)) + 1 ;

then lower_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . ((indx (D2,D1,n1)) + 1) by A261, A326, A327, INTEGRA1:def 4;

then A329: vol (divset (D2,((indx (D2,D1,n1)) + 2))) = (D1 . j) - (D2 . ((indx (D2,D1,n1)) + 1)) by A238, A328, INTEGRA1:def 5;

A330: upper_bound (divset (D1,(n1 + 1))) = D1 . (n1 + 1) by A245, A280, A268, A282, INTEGRA1:def 4;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A280, A268, A282, INTEGRA1:def 4;

then A331: vol (divset (D1,(n1 + 1))) = (D1 . (n1 + 1)) - (D1 . n1) by A330, INTEGRA1:def 5;

A332: vol (divset (D2,((indx (D2,D1,n1)) + 2))) >= 0 by INTEGRA1:9;

A333: indx (D2,D1,j) <= len H_{1}(D2)
by A263, INTEGRA1:def 7;

A334: vol (divset (D2,((indx (D2,D1,n1)) + 1))) >= 0 by INTEGRA1:9;

A335: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;

A336: (indx (D2,D1,n1)) + 1 <= (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then (indx (D2,D1,n1)) + 1 <= len D2 by A263, A326, XXREAL_0:2;

then A337: (indx (D2,D1,n1)) + 1 in dom D2 by A335, FINSEQ_3:25;

then H_{1}(D2) . ((indx (D2,D1,n1)) + 1) = (lower_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))
by INTEGRA1:def 7;

then A338: H_{1}(D2) . ((indx (D2,D1,n1)) + 1) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))
by A1, A337, A334, Th18, XREAL_1:64;

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 = 1 + 1 by A326;

then A339: (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 2 =
H_{1}(D2) . ((2 + ((indx (D2,D1,n1)) + 1)) - 1)
by A335, A336, A333, FINSEQ_6:122

.= H_{1}(D2) . (((indx (D2,D1,n1)) + 0) + 2)
;

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 >= 1 by A326;

then (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 1 =
H_{1}(D2) . ((1 + ((indx (D2,D1,n1)) + 1)) - 1)
by A326, A335, A336, A333, FINSEQ_6:122

.= H_{1}(D2) . ((indx (D2,D1,n1)) + 1)
;

then mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*(H_{1}(D2) . ((indx (D2,D1,n1)) + 1)),(H_{1}(D2) . ((indx (D2,D1,n1)) + 2))*>
by A316, A326, A339, FINSEQ_1:44;

then A340: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) = (H_{1}(D2) . ((indx (D2,D1,n1)) + 1)) + (H_{1}(D2) . ((indx (D2,D1,n1)) + 2))
by RVSUM_1:77;

A341: (indx (D2,D1,n1)) + 1 > 1 by A260, NAT_1:13;

then A342: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A337, INTEGRA1:def 4;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A337, A341, INTEGRA1:def 4;

then A343: vol (divset (D2,((indx (D2,D1,n1)) + 1))) = (D2 . ((indx (D2,D1,n1)) + 1)) - (D1 . n1) by A274, A342, INTEGRA1:def 5;

H_{1}(D2) . ((indx (D2,D1,n1)) + 2) = (lower_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 2))))
by A261, A326, INTEGRA1:def 7;

then H_{1}(D2) . ((indx (D2,D1,n1)) + 2) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 2))))
by A1, A261, A326, A332, Th18, XREAL_1:64;

then Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))) + ((upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 2)))))
by A340, A338, XREAL_1:7;

hence Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A282, A343, A329, A331; :: thesis: verum

end;then A327: (indx (D2,D1,n1)) + 2 <> 1 ;

then A328: upper_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . (indx (D2,D1,j)) by A261, A326, INTEGRA1:def 4;

((indx (D2,D1,n1)) + 2) - 1 = (indx (D2,D1,n1)) + 1 ;

then lower_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . ((indx (D2,D1,n1)) + 1) by A261, A326, A327, INTEGRA1:def 4;

then A329: vol (divset (D2,((indx (D2,D1,n1)) + 2))) = (D1 . j) - (D2 . ((indx (D2,D1,n1)) + 1)) by A238, A328, INTEGRA1:def 5;

A330: upper_bound (divset (D1,(n1 + 1))) = D1 . (n1 + 1) by A245, A280, A268, A282, INTEGRA1:def 4;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A280, A268, A282, INTEGRA1:def 4;

then A331: vol (divset (D1,(n1 + 1))) = (D1 . (n1 + 1)) - (D1 . n1) by A330, INTEGRA1:def 5;

A332: vol (divset (D2,((indx (D2,D1,n1)) + 2))) >= 0 by INTEGRA1:9;

A333: indx (D2,D1,j) <= len H

A334: vol (divset (D2,((indx (D2,D1,n1)) + 1))) >= 0 by INTEGRA1:9;

A335: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;

A336: (indx (D2,D1,n1)) + 1 <= (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then (indx (D2,D1,n1)) + 1 <= len D2 by A263, A326, XXREAL_0:2;

then A337: (indx (D2,D1,n1)) + 1 in dom D2 by A335, FINSEQ_3:25;

then H

then A338: H

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 = 1 + 1 by A326;

then A339: (mid (H

.= H

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 >= 1 by A326;

then (mid (H

.= H

then mid (H

then A340: Sum (mid (H

A341: (indx (D2,D1,n1)) + 1 > 1 by A260, NAT_1:13;

then A342: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A337, INTEGRA1:def 4;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A337, A341, INTEGRA1:def 4;

then A343: vol (divset (D2,((indx (D2,D1,n1)) + 1))) = (D2 . ((indx (D2,D1,n1)) + 1)) - (D1 . n1) by A274, A342, INTEGRA1:def 5;

H

then H

then Sum (mid (H

hence Sum (mid (H

then A345: len (mid (H

.= (j - j) + 1 by A282, XREAL_1:233

.= 1 ;

reconsider lv = (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) as Element of REAL by XREAL_0:def 1;

(n1 + 1) + 1 <= j + 1 by A257, XREAL_1:6;

then 1 <= (j + 1) - (n1 + 1) by XREAL_1:19;

then (mid (H

.= (lower_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) by A268, INTEGRA1:def 7 ;

then mid (H

then A346: Sum (mid (H

divset (D1,(n1 + 1)) c= A by A268, INTEGRA1:8;

then A347: lower_bound (rng (f | (divset (D1,(n1 + 1))))) >= lower_bound (rng f) by A1, Lm4;

n1 + 1 in Seg (len D1) by A268, FINSEQ_1:def 3;

then n1 + 1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;

then A348: n1 + 1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;

vol (divset (D1,(n1 + 1))) = (upper_volume ((chi (A,A)),D1)) . (n1 + 1) by A268, INTEGRA1:20;

then vol (divset (D1,(n1 + 1))) in rng (upper_volume ((chi (A,A)),D1)) by A348, FUNCT_1:def 3;

then A349: vol (divset (D1,(n1 + 1))) <= delta D1 by XXREAL_2:def 8;

(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;

then A350: ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,(n1 + 1)))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A349, XREAL_1:64;

vol (divset (D1,(n1 + 1))) >= 0 by INTEGRA1:9;

then Sum (mid (H

then (Sum (mid (H

hence (Sum (mid (H

suppose A351:
n1 + 1 < j
; :: thesis: (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) - (Sum (mid (H_{1}(D1),(n1 + 1),j))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

A352:
n1 < n1 + 1
by NAT_1:13;

then A353: D1 . n1 < D1 . (n1 + 1) by A241, A268, SEQM_3:def 1;

then consider B being non empty closed_interval Subset of REAL, MD1, MD2 being Division of B such that

A354: D1 . n1 = lower_bound B and

upper_bound B = MD2 . (len MD2) and

A355: upper_bound B = MD1 . (len MD1) and

A356: MD1 <= MD2 and

A357: MD1 = mid (D1,(n1 + 1),j) and

A358: MD2 = mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j))) by A13, A236, A257, A268, A273, Th15;

A359: delta MD1 >= 0 by Th9;

A360: len MD1 = (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;

then A361: ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A257, XREAL_1:233

.= j ;

j -' (n1 + 1) = j - (n1 + 1) by A257, XREAL_1:233;

then A362: (j -' (n1 + 1)) + 1 = j - n1 ;

then A363: len MD1 = j - n1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;

A364: B c= A

A371: len (lower_volume (g,MD1)) = len MD1 by INTEGRA1:def 7

.= (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118

.= (j - (n1 + 1)) + 1 by A257, XREAL_1:233 ;

A372: len MD1 in dom MD1 by FINSEQ_5:6;

then A373: 1 <= len MD1 by FINSEQ_3:25;

A374: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

A384: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A259, A274, A269, A271, SEQ_4:137;

then A385: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,(n1 + 1)) by NAT_1:13;

then A386: (indx (D2,D1,n1)) + 1 <= len D2 by A277, XXREAL_0:2;

vol B = (upper_bound B) - (D1 . n1) by A354, INTEGRA1:def 5;

then vol B = (D1 . j) - (D1 . n1) by A236, A245, A280, A355, A374, A384, INTEGRA1:def 4;

then A387: vol B <> 0 by A236, A241, A245, SEQM_3:def 1;

A388: 1 <= (indx (D2,D1,n1)) + 1 by A260, NAT_1:13;

A389: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A390: indx (D2,D1,(n1 + 1)) = (indx (D2,D1,n1)) + 1_{1}(D1)
by A266, INTEGRA1:def 7;

A408: for k being Nat st 1 <= k & k <= len (lower_volume (g,MD1)) holds

(lower_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k

then A439: lower_bound (rng f) <= lower_bound (rng g) by RELAT_1:70, SEQ_4:47;

rng f is bounded_above by A1, INTEGRA1:13;

then upper_bound (rng f) >= upper_bound (rng g) by RELAT_1:70, SEQ_4:48;

then (upper_bound (rng f)) - (lower_bound (rng f)) >= (upper_bound (rng g)) - (lower_bound (rng g)) by A439, XREAL_1:13;

then A440: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A359, XREAL_1:64;

A441: n1 < j - 1 by A351, XREAL_1:20;

A442: indx (D2,D1,j) <= len H_{1}(D2)
by A263, INTEGRA1:def 7;

A443: len MD2 = ((indx (D2,D1,j)) -' (indx (D2,D1,(n1 + 1)))) + 1 by A272, A270, A277, A262, A263, A358, FINSEQ_6:118;

then A444: len MD2 = ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by A272, XREAL_1:233;

then A445: len (lower_volume (g,MD2)) = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A390, INTEGRA1:def 7;

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

x1 in rng MD2

then A353: D1 . n1 < D1 . (n1 + 1) by A241, A268, SEQM_3:def 1;

then consider B being non empty closed_interval Subset of REAL, MD1, MD2 being Division of B such that

A354: D1 . n1 = lower_bound B and

upper_bound B = MD2 . (len MD2) and

A355: upper_bound B = MD1 . (len MD1) and

A356: MD1 <= MD2 and

A357: MD1 = mid (D1,(n1 + 1),j) and

A358: MD2 = mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j))) by A13, A236, A257, A268, A273, Th15;

A359: delta MD1 >= 0 by Th9;

A360: len MD1 = (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;

then A361: ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A257, XREAL_1:233

.= j ;

j -' (n1 + 1) = j - (n1 + 1) by A257, XREAL_1:233;

then A362: (j -' (n1 + 1)) + 1 = j - n1 ;

then A363: len MD1 = j - n1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;

A364: B c= A

proof

then reconsider g = f | B as Function of B,REAL by FUNCT_2:32;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in B or x1 in A )

A365: rng D1 c= A by INTEGRA1:def 2;

D1 . n1 in rng D1 by A241, FUNCT_1:def 3;

then A366: lower_bound A <= D1 . n1 by A365, INTEGRA2:1;

assume A367: x1 in B ; :: thesis: x1 in A

then reconsider x1 = x1 as Real ;

A368: x1 <= MD1 . (len MD1) by A355, A367, INTEGRA2:1;

D1 . j in rng D1 by A236, FUNCT_1:def 3;

then A369: D1 . j <= upper_bound A by A365, INTEGRA2:1;

D1 . n1 <= x1 by A354, A367, INTEGRA2:1;

then A370: lower_bound A <= x1 by A366, XXREAL_0:2;

MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A257, A281, A266, A244, A357, A362, A363, FINSEQ_6:122

.= D1 . j ;

then x1 <= upper_bound A by A368, A369, XXREAL_0:2;

hence x1 in A by A370, INTEGRA2:1; :: thesis: verum

end;A365: rng D1 c= A by INTEGRA1:def 2;

D1 . n1 in rng D1 by A241, FUNCT_1:def 3;

then A366: lower_bound A <= D1 . n1 by A365, INTEGRA2:1;

assume A367: x1 in B ; :: thesis: x1 in A

then reconsider x1 = x1 as Real ;

A368: x1 <= MD1 . (len MD1) by A355, A367, INTEGRA2:1;

D1 . j in rng D1 by A236, FUNCT_1:def 3;

then A369: D1 . j <= upper_bound A by A365, INTEGRA2:1;

D1 . n1 <= x1 by A354, A367, INTEGRA2:1;

then A370: lower_bound A <= x1 by A366, XXREAL_0:2;

MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A257, A281, A266, A244, A357, A362, A363, FINSEQ_6:122

.= D1 . j ;

then x1 <= upper_bound A by A368, A369, XXREAL_0:2;

hence x1 in A by A370, INTEGRA2:1; :: thesis: verum

A371: len (lower_volume (g,MD1)) = len MD1 by INTEGRA1:def 7

.= (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118

.= (j - (n1 + 1)) + 1 by A257, XREAL_1:233 ;

A372: len MD1 in dom MD1 by FINSEQ_5:6;

then A373: 1 <= len MD1 by FINSEQ_3:25;

A374: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

proof
end;

A383:
len MD1 in dom MD1
by FINSEQ_5:6;per cases
( len MD1 = 1 or len MD1 <> 1 )
;

end;

suppose A375:
len MD1 = 1
; :: thesis: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

then A376:
upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)
by A372, INTEGRA1:def 4;

A377: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

hence ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) ) by A265, A266, A354, A357, A361, A372, A375, A376, A377, FINSEQ_6:118, INTEGRA1:def 4; :: thesis: verum

end;A377: upper_bound (divset (D1,j)) = D1 . j by A236, A245, A280, INTEGRA1:def 4;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

hence ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) ) by A265, A266, A354, A357, A361, A372, A375, A376, A377, FINSEQ_6:118, INTEGRA1:def 4; :: thesis: verum

suppose A378:
len MD1 <> 1
; :: thesis: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

then
(len MD1) - 1 in dom MD1
by A372, INTEGRA1:7;

then A379: (len MD1) - 1 >= 1 by FINSEQ_3:25;

len MD1 <= (len MD1) + 1 by NAT_1:11;

then A380: (len MD1) - 1 <= len MD1 by XREAL_1:20;

upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A372, A378, INTEGRA1:def 4;

then A381: upper_bound (divset (MD1,(len MD1))) = D1 . j by A257, A266, A244, A357, A360, A361, A373, FINSEQ_6:122;

A382: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A363;

lower_bound (divset (MD1,(len MD1))) = MD1 . ((len MD1) - 1) by A372, A378, INTEGRA1:def 4;

then lower_bound (divset (MD1,(len MD1))) = D1 . (j - 1) by A257, A266, A244, A357, A360, A382, A379, A380, FINSEQ_6:122;

hence ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) ) by A236, A245, A280, A381, INTEGRA1:def 4; :: thesis: verum

end;then A379: (len MD1) - 1 >= 1 by FINSEQ_3:25;

len MD1 <= (len MD1) + 1 by NAT_1:11;

then A380: (len MD1) - 1 <= len MD1 by XREAL_1:20;

upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A372, A378, INTEGRA1:def 4;

then A381: upper_bound (divset (MD1,(len MD1))) = D1 . j by A257, A266, A244, A357, A360, A361, A373, FINSEQ_6:122;

A382: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A363;

lower_bound (divset (MD1,(len MD1))) = MD1 . ((len MD1) - 1) by A372, A378, INTEGRA1:def 4;

then lower_bound (divset (MD1,(len MD1))) = D1 . (j - 1) by A257, A266, A244, A357, A360, A382, A379, A380, FINSEQ_6:122;

hence ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) ) by A236, A245, A280, A381, INTEGRA1:def 4; :: thesis: verum

A384: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

proof
end;

D1 . n1 < D1 . (n1 + 1)
by A241, A268, A352, SEQM_3:def 1;per cases
( len MD1 = 1 or len MD1 <> 1 )
;

end;

suppose
len MD1 = 1
; :: thesis: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

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

end;suppose
len MD1 <> 1
; :: thesis: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

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

end;then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A259, A274, A269, A271, SEQ_4:137;

then A385: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,(n1 + 1)) by NAT_1:13;

then A386: (indx (D2,D1,n1)) + 1 <= len D2 by A277, XXREAL_0:2;

vol B = (upper_bound B) - (D1 . n1) by A354, INTEGRA1:def 5;

then vol B = (D1 . j) - (D1 . n1) by A236, A245, A280, A355, A374, A384, INTEGRA1:def 4;

then A387: vol B <> 0 by A236, A241, A245, SEQM_3:def 1;

A388: 1 <= (indx (D2,D1,n1)) + 1 by A260, NAT_1:13;

A389: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A390: indx (D2,D1,(n1 + 1)) = (indx (D2,D1,n1)) + 1

proof

A407:
j <= len H
assume
indx (D2,D1,(n1 + 1)) <> (indx (D2,D1,n1)) + 1
; :: thesis: contradiction

then A391: indx (D2,D1,(n1 + 1)) > (indx (D2,D1,n1)) + 1 by A385, XXREAL_0:1;

A392: (indx (D2,D1,n1)) + 1 in dom D2 by A388, A386, FINSEQ_3:25;

then A393: D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by FUNCT_1:def 3;

end;then A391: indx (D2,D1,(n1 + 1)) > (indx (D2,D1,n1)) + 1 by A385, XXREAL_0:1;

A392: (indx (D2,D1,n1)) + 1 in dom D2 by A388, A386, FINSEQ_3:25;

then A393: D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by FUNCT_1:def 3;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( D2 . ((indx (D2,D1,n1)) + 1) in rng D1 or D2 . ((indx (D2,D1,n1)) + 1) in rng D )
by A14, A393, XBOOLE_0:def 3;

end;

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

then consider n2 being Element of NAT such that

A394: n2 in dom D1 and

A395: D2 . ((indx (D2,D1,n1)) + 1) = D1 . n2 by PARTFUN1:3;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A259, A389, A392, SEQM_3:def 1;

then n1 < n2 by A241, A274, A394, A395, SEQ_4:137;

then A396: n1 + 1 <= n2 by NAT_1:13;

D1 . n2 < D1 . (n1 + 1) by A269, A271, A391, A392, A395, SEQM_3:def 1;

hence contradiction by A268, A394, A396, SEQ_4:137; :: thesis: verum

end;A394: n2 in dom D1 and

A395: D2 . ((indx (D2,D1,n1)) + 1) = D1 . n2 by PARTFUN1:3;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A259, A389, A392, SEQM_3:def 1;

then n1 < n2 by A241, A274, A394, A395, SEQ_4:137;

then A396: n1 + 1 <= n2 by NAT_1:13;

D1 . n2 < D1 . (n1 + 1) by A269, A271, A391, A392, A395, SEQM_3:def 1;

hence contradiction by A268, A394, A396, SEQ_4:137; :: thesis: verum

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

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

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

A400: n2 in dom D and

A401: D2 . ((indx (D2,D1,n1)) + 1) = D . n2 by A397, PARTFUN1:3;

D1 . n1 < D . n2 by A259, A274, A389, A392, A401, SEQM_3:def 1;

then D . i < D . n2 by A398, A399, XXREAL_0:2;

then i < n2 by A240, A400, SEQ_4:137;

then A402: i + 1 <= n2 by NAT_1:13;

(n1 + 1) + 1 <= j by A351, NAT_1:13;

then A403: n1 + 1 <= j - 1 by XREAL_1:19;

j - 1 in dom D1 by A236, A245, A280, INTEGRA1:7;

then A404: D1 . (n1 + 1) <= D1 . (j - 1) by A268, A403, SEQ_4:137;

A405: lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

then A406: D1 . (n1 + 1) <= D . (i + 1) by A404, A405, XXREAL_0:2;

D . n2 < D1 . (n1 + 1) by A269, A271, A391, A392, A401, SEQM_3:def 1;

then D . n2 < D . (i + 1) by A406, XXREAL_0:2;

hence contradiction by A235, A400, A402, SEQ_4:137; :: thesis: verum

end;A399: upper_bound (divset (D1,n1)) = D1 . n1

proof
end;

consider n2 being Element of NAT such that A400: n2 in dom D and

A401: D2 . ((indx (D2,D1,n1)) + 1) = D . n2 by A397, PARTFUN1:3;

D1 . n1 < D . n2 by A259, A274, A389, A392, A401, SEQM_3:def 1;

then D . i < D . n2 by A398, A399, XXREAL_0:2;

then i < n2 by A240, A400, SEQ_4:137;

then A402: i + 1 <= n2 by NAT_1:13;

(n1 + 1) + 1 <= j by A351, NAT_1:13;

then A403: n1 + 1 <= j - 1 by XREAL_1:19;

j - 1 in dom D1 by A236, A245, A280, INTEGRA1:7;

then A404: D1 . (n1 + 1) <= D1 . (j - 1) by A268, A403, SEQ_4:137;

A405: lower_bound (divset (D1,j)) <= D . (i + 1) by A237, INTEGRA2:1;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A236, A245, A280, INTEGRA1:def 4;

then A406: D1 . (n1 + 1) <= D . (i + 1) by A404, A405, XXREAL_0:2;

D . n2 < D1 . (n1 + 1) by A269, A271, A391, A392, A401, SEQM_3:def 1;

then D . n2 < D . (i + 1) by A406, XXREAL_0:2;

hence contradiction by A235, A400, A402, SEQ_4:137; :: thesis: verum

A408: for k being Nat st 1 <= k & k <= len (lower_volume (g,MD1)) holds

(lower_volume (g,MD1)) . k = (mid (H

proof

A431:
g | B is bounded
let k be Nat; :: thesis: ( 1 <= k & k <= len (lower_volume (g,MD1)) implies (lower_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k )

assume that

A409: 1 <= k and

A410: k <= len (lower_volume (g,MD1)) ; :: thesis: (lower_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k

k in Seg (len (lower_volume (g,MD1))) by A409, A410, FINSEQ_1:1;

then A411: k in Seg (len MD1) by INTEGRA1:def 7;

then A412: k in dom MD1 by FINSEQ_1:def 3;

k in dom MD1 by A411, FINSEQ_1:def 3;

then A413: (lower_volume (g,MD1)) . k = (lower_bound (rng (g | (divset (MD1,k))))) * (vol (divset (MD1,k))) by INTEGRA1:def 7;

consider k2 being Element of NAT such that

A414: n1 + 1 = 1 + k2 ;

A415: 1 <= k + k2 by A409, NAT_1:12;

k <= j - ((n1 + 1) - 1) by A371, A410;

then k + ((n1 + 1) - 1) <= j by XREAL_1:19;

then k + k2 <= len D1 by A266, A414, XXREAL_0:2;

then A416: k + k2 in Seg (len D1) by A415, FINSEQ_1:1;

then A417: k + k2 in dom D1 by FINSEQ_1:def 3;

1 + 1 <= k + k2 by A258, A409, A414, XREAL_1:7;

then A418: 1 < k + k2 by NAT_1:13;

A419: k2 = (n1 + 1) - 1 by A414;

A420: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )

then A428: divset (D1,(k + k2)) = divset (MD1,k) by A420, INTEGRA1:4;

A429: k + k2 in dom D1 by A416, FINSEQ_1:def 3;

A430: (mid (H_{1}(D1),(n1 + 1),j)) . k =
H_{1}(D1) . ((k + (n1 + 1)) - 1)
by A257, A244, A371, A407, A409, A410, FINSEQ_6:122

.= (lower_bound (rng (f | (divset (D1,(k + k2)))))) * (vol (divset (D1,(k + k2)))) by A414, A429, INTEGRA1:def 7 ;

k in dom MD1 by A411, FINSEQ_1:def 3;

then divset (D1,(k + k2)) c= B by A428, INTEGRA1:8;

hence (lower_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k
by A413, A430, A428, FUNCT_1:51; :: thesis: verum

end;assume that

A409: 1 <= k and

A410: k <= len (lower_volume (g,MD1)) ; :: thesis: (lower_volume (g,MD1)) . k = (mid (H

k in Seg (len (lower_volume (g,MD1))) by A409, A410, FINSEQ_1:1;

then A411: k in Seg (len MD1) by INTEGRA1:def 7;

then A412: k in dom MD1 by FINSEQ_1:def 3;

k in dom MD1 by A411, FINSEQ_1:def 3;

then A413: (lower_volume (g,MD1)) . k = (lower_bound (rng (g | (divset (MD1,k))))) * (vol (divset (MD1,k))) by INTEGRA1:def 7;

consider k2 being Element of NAT such that

A414: n1 + 1 = 1 + k2 ;

A415: 1 <= k + k2 by A409, NAT_1:12;

k <= j - ((n1 + 1) - 1) by A371, A410;

then k + ((n1 + 1) - 1) <= j by XREAL_1:19;

then k + k2 <= len D1 by A266, A414, XXREAL_0:2;

then A416: k + k2 in Seg (len D1) by A415, FINSEQ_1:1;

then A417: k + k2 in dom D1 by FINSEQ_1:def 3;

1 + 1 <= k + k2 by A258, A409, A414, XREAL_1:7;

then A418: 1 < k + k2 by NAT_1:13;

A419: k2 = (n1 + 1) - 1 by A414;

A420: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )

proof
end;

divset (MD1,k) = [.(lower_bound (divset (MD1,k))),(upper_bound (divset (MD1,k))).]
by INTEGRA1:4;per cases
( k = 1 or k <> 1 )
;

end;

suppose A421:
k = 1
; :: thesis: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )

then
upper_bound (divset (MD1,k)) = MD1 . k
by A412, INTEGRA1:def 4;

then A422: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A371, A409, A410, FINSEQ_6:122;

lower_bound (divset (MD1,k)) = D1 . n1 by A354, A412, A421, INTEGRA1:def 4;

hence ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) ) by A419, A418, A417, A421, A422, INTEGRA1:def 4; :: thesis: verum

end;then A422: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A371, A409, A410, FINSEQ_6:122;

lower_bound (divset (MD1,k)) = D1 . n1 by A354, A412, A421, INTEGRA1:def 4;

hence ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) ) by A419, A418, A417, A421, A422, INTEGRA1:def 4; :: thesis: verum

suppose A423:
k <> 1
; :: thesis: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )

then
upper_bound (divset (MD1,k)) = MD1 . k
by A412, INTEGRA1:def 4;

then A424: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A371, A409, A410, FINSEQ_6:122;

A425: k - 1 <= (j - (n1 + 1)) + 1 by A371, A410, XREAL_1:146, XXREAL_0:2;

A426: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A412, A423, INTEGRA1:def 4;

A427: k - 1 in dom MD1 by A412, A423, INTEGRA1:7;

then 1 <= k - 1 by FINSEQ_3:25;

then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A257, A266, A244, A357, A427, A425, A426, FINSEQ_6:122;

hence ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) ) by A414, A418, A417, A424, INTEGRA1:def 4; :: thesis: verum

end;then A424: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A257, A266, A244, A357, A371, A409, A410, FINSEQ_6:122;

A425: k - 1 <= (j - (n1 + 1)) + 1 by A371, A410, XREAL_1:146, XXREAL_0:2;

A426: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A412, A423, INTEGRA1:def 4;

A427: k - 1 in dom MD1 by A412, A423, INTEGRA1:7;

then 1 <= k - 1 by FINSEQ_3:25;

then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A257, A266, A244, A357, A427, A425, A426, FINSEQ_6:122;

hence ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) ) by A414, A418, A417, A424, INTEGRA1:def 4; :: thesis: verum

then A428: divset (D1,(k + k2)) = divset (MD1,k) by A420, INTEGRA1:4;

A429: k + k2 in dom D1 by A416, FINSEQ_1:def 3;

A430: (mid (H

.= (lower_bound (rng (f | (divset (D1,(k + k2)))))) * (vol (divset (D1,(k + k2)))) by A414, A429, INTEGRA1:def 7 ;

k in dom MD1 by A411, FINSEQ_1:def 3;

then divset (D1,(k + k2)) c= B by A428, INTEGRA1:8;

hence (lower_volume (g,MD1)) . k = (mid (H

proof

rng f is bounded_below
by A1, INTEGRA1:11;
consider a being Real such that

A432: for x being object st x in A /\ (dom f) holds

a <= f . x by A1, RFUNCT_1:71;

for x being object st x in B /\ (dom g) holds

a <= g . x

consider a being Real such that

A436: for x being object st x in A /\ (dom f) holds

f . x <= a by A1, RFUNCT_1:70;

for x being object st x in B /\ (dom g) holds

g . x <= a

hence g | B is bounded by A435; :: thesis: verum

end;A432: for x being object st x in A /\ (dom f) holds

a <= f . x by A1, RFUNCT_1:71;

for x being object st x in B /\ (dom g) holds

a <= g . x

proof

then A435:
g | B is bounded_below
by RFUNCT_1:71;
let x be object ; :: thesis: ( x in B /\ (dom g) implies a <= g . x )

A433: (dom f) /\ B c= (dom f) /\ A by A364, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: a <= g . x

then A434: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a <= f . x by A432, A433;

hence a <= g . x by A434, FUNCT_1:47; :: thesis: verum

end;A433: (dom f) /\ B c= (dom f) /\ A by A364, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: a <= g . x

then A434: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a <= f . x by A432, A433;

hence a <= g . x by A434, FUNCT_1:47; :: thesis: verum

consider a being Real such that

A436: for x being object st x in A /\ (dom f) holds

f . x <= a by A1, RFUNCT_1:70;

for x being object st x in B /\ (dom g) holds

g . x <= a

proof

then
g | B is bounded_above
by RFUNCT_1:70;
let x be object ; :: thesis: ( x in B /\ (dom g) implies g . x <= a )

A437: (dom f) /\ B c= (dom f) /\ A by A364, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: g . x <= a

then A438: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a >= f . x by A436, A437;

hence g . x <= a by A438, FUNCT_1:47; :: thesis: verum

end;A437: (dom f) /\ B c= (dom f) /\ A by A364, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: g . x <= a

then A438: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a >= f . x by A436, A437;

hence g . x <= a by A438, FUNCT_1:47; :: thesis: verum

hence g | B is bounded by A435; :: thesis: verum

then A439: lower_bound (rng f) <= lower_bound (rng g) by RELAT_1:70, SEQ_4:47;

rng f is bounded_above by A1, INTEGRA1:13;

then upper_bound (rng f) >= upper_bound (rng g) by RELAT_1:70, SEQ_4:48;

then (upper_bound (rng f)) - (lower_bound (rng f)) >= (upper_bound (rng g)) - (lower_bound (rng g)) by A439, XREAL_1:13;

then A440: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A359, XREAL_1:64;

A441: n1 < j - 1 by A351, XREAL_1:20;

A442: indx (D2,D1,j) <= len H

A443: len MD2 = ((indx (D2,D1,j)) -' (indx (D2,D1,(n1 + 1)))) + 1 by A272, A270, A277, A262, A263, A358, FINSEQ_6:118;

then A444: len MD2 = ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by A272, XREAL_1:233;

then A445: len (lower_volume (g,MD2)) = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A390, INTEGRA1:def 7;

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

x1 in rng MD2

proof

let x1 be object ; :: thesis: ( x1 in (rng MD1) \/ {(D . (i + 1))} implies x1 in rng MD2 )

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

then reconsider x1 = x1 as Real ;

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

then reconsider x1 = x1 as Real ;

now :: thesis: x1 in rng MD2

per cases
( x1 in rng MD1 or x1 in {(D . (i + 1))} )
by A446, XBOOLE_0:def 3;

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

rng MD1 <> {}
;

then 1 in dom MD1 by FINSEQ_3:32;

then A448: 1 <= len MD1 by FINSEQ_3:25;

rng MD1 c= rng D1 by A357, FINSEQ_6:119;

then A449: x1 in rng D1 by A447;

rng D1 c= rng D2 by A13, INTEGRA1:def 18;

then consider k being Element of NAT such that

A450: k in dom D2 and

A451: D2 . k = x1 by A449, PARTFUN1:3;

MD1 . 1 = D1 . (n1 + 1) by A265, A266, A244, A267, A357, FINSEQ_6:118;

then D2 . (indx (D2,D1,(n1 + 1))) <= x1 by A271, A447, Th16;

then A452: indx (D2,D1,(n1 + 1)) <= k by A269, A450, A451, SEQM_3:def 1;

then consider n being Nat such that

A453: k + 1 = (indx (D2,D1,(n1 + 1))) + n by NAT_1:10, NAT_1:12;

A454: len MD1 = (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;

then ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A257, XREAL_1:233

.= j ;

then MD1 . (len MD1) = D1 . j by A257, A266, A244, A357, A448, A454, FINSEQ_6:122;

then x1 <= D2 . (indx (D2,D1,j)) by A238, A447, Th16;

then k <= indx (D2,D1,j) by A261, A450, A451, SEQM_3:def 1;

then k - (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1))) by XREAL_1:9;

then A455: (k - (indx (D2,D1,(n1 + 1)))) + 1 <= ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by XREAL_1:6;

(indx (D2,D1,(n1 + 1)))

then 1 in dom MD1 by FINSEQ_3:32;

then A448: 1 <= len MD1 by FINSEQ_3:25;

rng MD1 c= rng D1 by A357, FINSEQ_6:119;

then A449: x1 in rng D1 by A447;

rng D1 c= rng D2 by A13, INTEGRA1:def 18;

then consider k being Element of NAT such that

A450: k in dom D2 and

A451: D2 . k = x1 by A449, PARTFUN1:3;

MD1 . 1 = D1 . (n1 + 1) by A265, A266, A244, A267, A357, FINSEQ_6:118;

then D2 . (indx (D2,D1,(n1 + 1))) <= x1 by A271, A447, Th16;

then A452: indx (D2,D1,(n1 + 1)) <= k by A269, A450, A451, SEQM_3:def 1;

then consider n being Nat such that

A453: k + 1 = (indx (D2,D1,(n1 + 1))) + n by NAT_1:10, NAT_1:12;

A454: len MD1 = (j -' (n1 + 1)) + 1 by A257, A265, A266, A244, A267, A357, FINSEQ_6:118;

then ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A257, XREAL_1:233

.= j ;

then MD1 . (len MD1) = D1 . j by A257, A266, A244, A357, A448, A454, FINSEQ_6:122;

then x1 <= D2 . (indx (D2,D1,j)) by A238, A447, Th16;

then k <= indx (D2,D1,j) by A261, A450, A451, SEQM_3:def 1;

then k - (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1))) by XREAL_1:9;

then A455: (k - (indx (D2,D1,(n1 + 1)))) + 1 <= ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by XREAL_1:6;

(indx (D2,D1,(n1 + 1)))