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

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

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

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

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

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

ex D2 being Division of A st

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

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

ex D2 being Division of A st

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

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

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

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

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

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

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

ex D2 being Division of A st

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

proof

consider D2 being Division of A such that

A9: D <= D2 and

A10: D1 <= D2 and

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

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

0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) by A2;

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

A9: D <= D2 and

A10: D1 <= D2 and

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

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

0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) by A2;

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

proof

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

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

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

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

ex j being Element of NAT st

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

deffunc H

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

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

ex j being Element of NAT st

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

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}(D1,j) - H_{2}(D2, indx (D2,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}(D1,j) - H_{2}(D2, indx (D2,D1,j)) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) )

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

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

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

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

j >= 2_{1}[1]

A227: 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 A14: i in dom D ; :: thesis: ex j being Element of NAT st

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

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

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

j >= 2

proof

A36:
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 A17: i in dom D ; :: thesis: ( not j in dom D1 or not D . i in divset (D1,j) or j >= 2 )

assume that

A18: j in dom D1 and

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

assume j < 2 ; :: thesis: contradiction

then j < 1 + 1 ;

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

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

then j >= 1 by FINSEQ_1:1;

then j = 1 by A20, XXREAL_0:1;

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

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

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

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

assume that

A18: j in dom D1 and

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

assume j < 2 ; :: thesis: contradiction

then j < 1 + 1 ;

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

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

then j >= 1 by FINSEQ_1:1;

then j = 1 by A20, XXREAL_0:1;

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

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

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

proof
end;

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

end;

suppose A23:
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 A24: 1 in dom D by FINSEQ_3:25;

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

1 in Seg (len D) by A24, FINSEQ_1:def 3;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1 in Seg (len D) by A24, FINSEQ_1:def 3;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

upper_bound (divset (D,i)) = D . i by A17, A30, INTEGRA1:def 4;

then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound A) by A22, A21, 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 A32, XXREAL_0:2;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

upper_bound (divset (D,i)) = D . i by A17, A30, INTEGRA1:def 4;

then (upper_bound (divset (D1,j))) - (lower_bound (divset (D1,j))) >= (upper_bound (divset (D,i))) - (lower_bound A) by A22, A21, 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 A32, XXREAL_0:2;

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

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

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

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

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

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

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

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

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

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

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

proof

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

then 1 <= len D by FINSEQ_1:1;

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

then consider j being Element of NAT such that

A38: j in dom D1 and

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

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

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

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

then consider j being Element of NAT such that

A38: j in dom D1 and

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

H

proof

hence
S
A40:
j <> 1
by A16, A37, A38, A39;

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

A41: j1 in dom D1 by A38, A40, INTEGRA1:7;

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

then j1 in Seg (len (upper_volume (f,D1))) by INTEGRA1:def 6;

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

A43: j - 1 in dom D1 by A38, A40, INTEGRA1:7;

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

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

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

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

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

j < j + 1 by NAT_1:13;

then j1 < j by XREAL_1:19;

then A48: indx (D2,D1,j1) < indx (D2,D1,j) by A10, A38, A41, Th8;

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

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

then A127: j1 < j by XREAL_1:19;

indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

A130: indx (D2,D1,j1) <= len D2 by A45, FINSEQ_1:1;

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

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

then A133: 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)))

A146: 1 <= j1 by A132, FINSEQ_1:1;

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

then A147: D1 . j1 <= D . 1 by A38, A40, INTEGRA1:def 4;

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

x1 in rng (D1 | j1)

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

mid (D1,1,j1) is increasing by A38, A40, A146, INTEGRA1:7, INTEGRA1:35;

then A167: D1 | j1 is increasing by A146, FINSEQ_6:116;

then A168: D2 | (indx (D2,D1,j1)) = D1 | j1 by A47, A166, Th6;

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

k = indx (D2,D1,k)

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

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

then A216: indx (D2,D1,j1) <= len (upper_volume (f,D2)) by INTEGRA1:def 6;

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

then A217: j1 <= len (upper_volume (f,D1)) by INTEGRA1:def 6;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A47, A167, A166, Th6;

then indx (D2,D1,j1) = j1 by A133, A131, FINSEQ_1:59;

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

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

then A218: (upper_volume (f,D2)) | (indx (D2,D1,j1)) = (upper_volume (f,D1)) | j1 by A187, FINSEQ_1:14;

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

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

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

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

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

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

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

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

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

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

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

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

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 A146, FINSEQ_6:116

.= Sum (mid (H_{1}(D1),1,j))
by A146, A224, A127, INTEGRA2:4

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

then A225: H_{2}(D1,j1) + (Sum (mid ((upper_volume (f,D1)),j,j))) = H_{2}(D1,j)
by A223, INTEGRA1:def 20;

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

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

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 ((upper_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 A46, FINSEQ_6:116

.= Sum (mid (H_{1}(D2),1,(indx (D2,D1,j))))
by A46, A48, A222, INTEGRA2:4

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

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

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

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

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

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

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

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

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

A41: j1 in dom D1 by A38, A40, INTEGRA1:7;

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

then j1 in Seg (len (upper_volume (f,D1))) by INTEGRA1:def 6;

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

A43: j - 1 in dom D1 by A38, A40, INTEGRA1:7;

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

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

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

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

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

j < j + 1 by NAT_1:13;

then j1 < j by XREAL_1:19;

then A48: indx (D2,D1,j1) < indx (D2,D1,j) by A10, A38, A41, Th8;

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

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

proof

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

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

then A79: j <= len (upper_volume (f,D1)) by INTEGRA1:def 6;

A80: 1 <= j by A38, FINSEQ_3:25;

then A81: (mid ((upper_volume (f,D1)),j,j)) . 1 = (upper_volume (f,D1)) . j by A79, FINSEQ_6:118;

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

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

then len (mid ((upper_volume (f,D1)),j,j)) = 1 by A80, A79, FINSEQ_6:118;

then mid ((upper_volume (f,D1)),j,j) = <*uv*> by A81, FINSEQ_1:40;

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

indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

indx (D2,D1,j) in Seg (len (upper_volume (f,D2))) by A83, INTEGRA1:def 6;

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

then A86: (indx (D2,D1,j1)) + 1 <= len (upper_volume (f,D2)) by A49, XXREAL_0:2;

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

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

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

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

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

then A89: len (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= 2 by A49, A84, A85, A78, A86, FINSEQ_6:118;

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

then A90: 1 <= len (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) by A49, A84, A85, A78, A86, FINSEQ_6:118;

end;proof

A78:
1 <= (indx (D2,D1,j1)) + 1
by A46, 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 A52: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,j) by XREAL_1:20;

A53: ID1 < ID2 by NAT_1:13;

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

then A54: 1 <= ID2 by A46, XXREAL_0:2;

A55: indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

then A57: ID2 in dom D2 by A54, FINSEQ_3:25;

then A58: D2 . ID2 < D2 . (indx (D2,D1,j)) by A52, A55, SEQM_3:def 1;

A59: 1 <= ID1 by A46, NAT_1:13;

A60: D1 . j = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

ID1 <= indx (D2,D1,j) by A52, A53, XXREAL_0:2;

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

then A61: ID1 in dom D2 by A59, FINSEQ_3:25;

then A62: D2 . ID1 < D2 . ID2 by A53, A57, SEQM_3:def 1;

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

then A63: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A44, A61, SEQM_3:def 1;

A64: D1 . j1 = D2 . (indx (D2,D1,j1)) by A10, A41, INTEGRA1:def 19;

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

then A73: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

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

then A74: lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A10, A41, INTEGRA1:def 19;

D2 . ID2 in rng D2 by A57, FUNCT_1:def 3;

then A75: D2 . ID2 in rng D by A11, A65, XBOOLE_0:def 3;

D2 . ID1 in rng D2 by A61, FUNCT_1:def 3;

then A76: D2 . ID1 in rng D by A11, A65, XBOOLE_0:def 3;

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

then D2 . ID2 in divset (D1,j) by A58, A74, A73, INTEGRA2:1;

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

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

then D2 . ID1 in divset (D1,j) by A63, A74, A73, INTEGRA2:1;

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

hence contradiction by A8, A38, A53, A61, A57, A77, 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 A52: (indx (D2,D1,j1)) + (1 + 1) < indx (D2,D1,j) by XREAL_1:20;

A53: ID1 < ID2 by NAT_1:13;

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

then A54: 1 <= ID2 by A46, XXREAL_0:2;

A55: indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

then A57: ID2 in dom D2 by A54, FINSEQ_3:25;

then A58: D2 . ID2 < D2 . (indx (D2,D1,j)) by A52, A55, SEQM_3:def 1;

A59: 1 <= ID1 by A46, NAT_1:13;

A60: D1 . j = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

ID1 <= indx (D2,D1,j) by A52, A53, XXREAL_0:2;

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

then A61: ID1 in dom D2 by A59, FINSEQ_3:25;

then A62: D2 . ID1 < D2 . ID2 by A53, A57, SEQM_3:def 1;

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

then A63: D2 . (indx (D2,D1,j1)) < D2 . ID1 by A44, A61, SEQM_3:def 1;

A64: D1 . j1 = D2 . (indx (D2,D1,j1)) by A10, A41, INTEGRA1:def 19;

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

proof

upper_bound (divset (D1,j)) = D1 . j
by A38, A40, INTEGRA1:def 4;
assume A66:
( 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 A66;

end;

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

then consider n being Element of NAT such that

A67: n in dom D1 and

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

j1 < n by A41, A63, A64, A67, A68, SEQ_4:137;

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

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

then n < j by A38, A60, A67, A68, SEQ_4:137;

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

end;A67: n in dom D1 and

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

j1 < n by A41, A63, A64, A67, A68, SEQ_4:137;

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

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

then n < j by A38, A60, A67, A68, SEQ_4:137;

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

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

then consider n being Element of NAT such that

A70: n in dom D1 and

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

D2 . (indx (D2,D1,j1)) < D2 . ID2 by A63, A62, XXREAL_0:2;

then j1 < n by A41, A64, A70, A71, SEQ_4:137;

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

n < j by A38, A58, A60, A70, A71, SEQ_4:137;

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

end;A70: n in dom D1 and

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

D2 . (indx (D2,D1,j1)) < D2 . ID2 by A63, A62, XXREAL_0:2;

then j1 < n by A41, A64, A70, A71, SEQ_4:137;

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

n < j by A38, A58, A60, A70, A71, SEQ_4:137;

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

then A73: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

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

then A74: lower_bound (divset (D1,j)) = D2 . (indx (D2,D1,j1)) by A10, A41, INTEGRA1:def 19;

D2 . ID2 in rng D2 by A57, FUNCT_1:def 3;

then A75: D2 . ID2 in rng D by A11, A65, XBOOLE_0:def 3;

D2 . ID1 in rng D2 by A61, FUNCT_1:def 3;

then A76: D2 . ID1 in rng D by A11, A65, XBOOLE_0:def 3;

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

then D2 . ID2 in divset (D1,j) by A58, A74, A73, INTEGRA2:1;

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

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

then D2 . ID1 in divset (D1,j) by A63, A74, A73, INTEGRA2:1;

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

hence contradiction by A8, A38, A53, A61, A57, A77, Th5, SEQ_4:138; :: thesis: verum

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

then A79: j <= len (upper_volume (f,D1)) by INTEGRA1:def 6;

A80: 1 <= j by A38, FINSEQ_3:25;

then A81: (mid ((upper_volume (f,D1)),j,j)) . 1 = (upper_volume (f,D1)) . j by A79, FINSEQ_6:118;

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

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

then len (mid ((upper_volume (f,D1)),j,j)) = 1 by A80, A79, FINSEQ_6:118;

then mid ((upper_volume (f,D1)),j,j) = <*uv*> by A81, FINSEQ_1:40;

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

indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

indx (D2,D1,j) in Seg (len (upper_volume (f,D2))) by A83, INTEGRA1:def 6;

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

then A86: (indx (D2,D1,j1)) + 1 <= len (upper_volume (f,D2)) by A49, XXREAL_0:2;

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

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

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

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

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

then A89: len (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) <= 2 by A49, A84, A85, A78, A86, FINSEQ_6:118;

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

then A90: 1 <= len (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) by A49, A84, A85, A78, A86, FINSEQ_6:118;

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

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

end;

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

upper_bound (divset (D1,j)) = D1 . j
by A38, A40, INTEGRA1:def 4;

then A92: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

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

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

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

A94: delta D1 >= 0 by Th9;

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

A96: indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

len (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = ((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 by A49, A84, A85, A78, A86, FINSEQ_6:118;

then A97: (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) = 0 by A49, A91, XREAL_1:233;

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

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

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

then lower_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j1)) by A46, A97, A96, INTEGRA1:def 4;

then A99: divset (D2,(indx (D2,D1,j))) = divset (D1,j) by A93, A98, INTEGRA1:4;

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

(mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (upper_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by A84, A85, A78, A86, FINSEQ_6:118;

then mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*uv*> by A91, FINSEQ_1:40;

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

.= (upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A88, INTEGRA1:def 6

.= Sum (mid ((upper_volume (f,D1)),j,j)) by A38, A82, A97, A99, INTEGRA1:def 6 ;

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

end;then A92: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

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

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

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

A94: delta D1 >= 0 by Th9;

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

A96: indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

len (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) = ((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 by A49, A84, A85, A78, A86, FINSEQ_6:118;

then A97: (indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1) = 0 by A49, A91, XREAL_1:233;

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

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

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

then lower_bound (divset (D2,(indx (D2,D1,j)))) = D2 . (indx (D2,D1,j1)) by A46, A97, A96, INTEGRA1:def 4;

then A99: divset (D2,(indx (D2,D1,j))) = divset (D1,j) by A93, A98, INTEGRA1:4;

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

(mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (upper_volume (f,D2)) . ((indx (D2,D1,j1)) + 1) by A84, A85, A78, A86, FINSEQ_6:118;

then mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))) = <*uv*> by A91, FINSEQ_1:40;

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

.= (upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A88, INTEGRA1:def 6

.= Sum (mid ((upper_volume (f,D1)),j,j)) by A38, A82, A97, A99, INTEGRA1:def 6 ;

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

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

A101:
(mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 1 = (upper_volume (f,D2)) . ((indx (D2,D1,j1)) + 1)
by A84, A85, A78, A86, FINSEQ_6:118;

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

(mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) . 2 = H_{1}(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1)
by A49, A84, A85, A78, A86, A100, FINSEQ_6:118

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

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

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

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

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

upper_bound (divset (D1,j)) = D1 . j by A38, A40, INTEGRA1:def 4;

then A105: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

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

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A49, A84, A85, A78, A86, A100, FINSEQ_6:118;

then A107: 2 = ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 by A49, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,j1)) ;

then A108: (indx (D2,D1,j1)) + 2 in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

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

(indx (D2,D1,j1)) + 1 in Seg (len (upper_volume (f,D2))) by A78, A86, FINSEQ_1:1;

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

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

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

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

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

then A113: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A110, A111, INTEGRA1:def 4;

A114: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A78, NAT_1:13;

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

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

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A108, A114, 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 A115, A109, 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 A113, A112 ;

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

then A117: (upper_volume (f,D1)) . j = (upper_bound (rng (f | (divset (D1,j))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A38, INTEGRA1:def 6;

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

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

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

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

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

.= H

.= H

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

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

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

upper_bound (divset (D1,j)) = D1 . j by A38, A40, INTEGRA1:def 4;

then A105: upper_bound (divset (D1,j)) = D2 . (indx (D2,D1,j)) by A10, A38, INTEGRA1:def 19;

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

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A49, A84, A85, A78, A86, A100, FINSEQ_6:118;

then A107: 2 = ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 by A49, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,j1)) ;

then A108: (indx (D2,D1,j1)) + 2 in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

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

(indx (D2,D1,j1)) + 1 in Seg (len (upper_volume (f,D2))) by A78, A86, FINSEQ_1:1;

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

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

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

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

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

then A113: lower_bound (divset (D2,((indx (D2,D1,j1)) + 1))) = D2 . (indx (D2,D1,j1)) by A110, A111, INTEGRA1:def 4;

A114: ((indx (D2,D1,j1)) + 1) + 1 > 1 by A78, NAT_1:13;

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

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

upper_bound (divset (D2,((indx (D2,D1,j1)) + 2))) = D2 . ((indx (D2,D1,j1)) + 2) by A108, A114, 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 A115, A109, 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 A113, A112 ;

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

then A117: (upper_volume (f,D1)) . j = (upper_bound (rng (f | (divset (D1,j))))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 1)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) by A38, INTEGRA1:def 6;

A118: (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 SR = upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))));

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

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

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

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

then A119: upper_bound (rng (f | (divset (D1,j)))) <= upper_bound (rng f) by A1, Lm4;

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

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

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

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

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A49, A84, A85, A78, A86, A100, FINSEQ_6:118;

then A121: 2 = ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 by A49, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,j1)) ;

A122: indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

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

A124: ((upper_volume (f,D1)) . j) - (A * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = A * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A117;

(upper_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A106, A119, XREAL_1:64;

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

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

(upper_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A104, A119, XREAL_1:64;

then (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))))
by A125, XXREAL_0:2;

then A126: 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)))))
by XREAL_1:20;

Sum (mid (H_{1}(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j)))) =
((upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + (H_{1}(D2) . ((indx (D2,D1,j1)) + 1))
by A103, A122, A121, INTEGRA1:def 6

.= ((upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A88, INTEGRA1:def 6 ;

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

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

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

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

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

then (Sum (mid (H_{1}(D1),j,j))) - (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)))))) - (((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))))
by A126, XREAL_1:13;

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

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

set SR = upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))));

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

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

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

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

then A119: upper_bound (rng (f | (divset (D1,j)))) <= upper_bound (rng f) by A1, Lm4;

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

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

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

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

((indx (D2,D1,j)) -' ((indx (D2,D1,j1)) + 1)) + 1 = 2 by A49, A84, A85, A78, A86, A100, FINSEQ_6:118;

then A121: 2 = ((indx (D2,D1,j)) - ((indx (D2,D1,j1)) + 1)) + 1 by A49, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,j1)) ;

A122: indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

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

A124: ((upper_volume (f,D1)) . j) - (A * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = A * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A117;

(upper_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A106, A119, XREAL_1:64;

then Sum (mid (H

then A125: (Sum (mid (H

(upper_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 1)))) by A104, A119, XREAL_1:64;

then (Sum (mid (H

then A126: Sum (mid (H

Sum (mid (H

.= ((upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2))))) + ((upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) by A88, INTEGRA1:def 6 ;

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 A38, Lm5, XREAL_1:64;

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

then A127: j1 < j by XREAL_1:19;

indx (D2,D1,j) in dom D2 by A10, A38, INTEGRA1:def 19;

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

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

A130: indx (D2,D1,j1) <= len D2 by A45, FINSEQ_1:1;

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

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

then A133: 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 A145:
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

A134: k in dom (D1 | j1) and

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

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

then A136: k in Seg j1 by A133, FINSEQ_1:59;

then A137: k in dom D1 by A41, RFINSEQ:6;

k <= j1 by A136, FINSEQ_1:1;

then D1 . k <= D1 . j1 by A43, A137, SEQ_4:137;

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

then A138: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by A10, A43, INTEGRA1:def 19;

A139: (D1 | j1) . k = D1 . k by A41, A136, RFINSEQ:6;

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

then x1 in rng D2 by A11, A135, A139, XBOOLE_0:def 3;

then consider n being Element of NAT such that

A140: n in dom D2 and

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

D2 . (indx (D2,D1,k)) = D2 . n by A10, A135, A139, A137, A141, INTEGRA1:def 19;

then A142: n <= indx (D2,D1,j1) by A44, A140, A138, SEQM_3:def 1;

1 <= n by A140, FINSEQ_3:25;

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

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

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

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

hence x1 in rng (D2 | (indx (D2,D1,j1))) by A141, A144, 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

A134: k in dom (D1 | j1) and

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

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

then A136: k in Seg j1 by A133, FINSEQ_1:59;

then A137: k in dom D1 by A41, RFINSEQ:6;

k <= j1 by A136, FINSEQ_1:1;

then D1 . k <= D1 . j1 by A43, A137, SEQ_4:137;

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

then A138: D2 . (indx (D2,D1,k)) <= D2 . (indx (D2,D1,j1)) by A10, A43, INTEGRA1:def 19;

A139: (D1 | j1) . k = D1 . k by A41, A136, RFINSEQ:6;

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

then x1 in rng D2 by A11, A135, A139, XBOOLE_0:def 3;

then consider n being Element of NAT such that

A140: n in dom D2 and

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

D2 . (indx (D2,D1,k)) = D2 . n by A10, A135, A139, A137, A141, INTEGRA1:def 19;

then A142: n <= indx (D2,D1,j1) by A44, A140, A138, SEQM_3:def 1;

1 <= n by A140, FINSEQ_3:25;

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

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

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

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

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

A146: 1 <= j1 by A132, FINSEQ_1:1;

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

then A147: D1 . j1 <= D . 1 by A38, A40, 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

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

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

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

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

then A151: k in dom D2 by A44, RFINSEQ:6;

A152: len (D1 | j1) = j1 by A133, FINSEQ_1:59;

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

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

then A153: D2 . k <= D1 . j1 by A10, A43, INTEGRA1:def 19;

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

hence x1 in rng (D1 | j1) by A11, A44, A149, A150, A163, A154, 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

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

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

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

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

then A151: k in dom D2 by A44, RFINSEQ:6;

A152: len (D1 | j1) = j1 by A133, FINSEQ_1:59;

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

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

then A153: D2 . k <= D1 . j1 by A10, A43, INTEGRA1:def 19;

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

proof

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

A155: m in dom D1 and

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

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

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

A158: m <= j1 by A41, A153, A155, A156, SEQM_3:def 1;

then m in Seg (len (D1 | j1)) by A152, A157, FINSEQ_1:1;

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

m in Seg j1 by A157, A158, FINSEQ_1:1;

then D2 . k = (D1 | j1) . m by A41, A156, RFINSEQ:6;

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

end;then consider m being Element of NAT such that

A155: m in dom D1 and

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

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

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

A158: m <= j1 by A41, A153, A155, A156, SEQM_3:def 1;

then m in Seg (len (D1 | j1)) by A152, A157, FINSEQ_1:1;

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

m in Seg j1 by A157, A158, FINSEQ_1:1;

then D2 . k = (D1 | j1) . m by A41, A156, RFINSEQ:6;

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

proof

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

A161: n in dom D and

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

1 <= n by A161, FINSEQ_3:25;

then D . 1 <= D2 . k by A37, A161, A162, SEQ_4:137;

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

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

end;then consider n being Element of NAT such that

A161: n in dom D and

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

1 <= n by A161, FINSEQ_3:25;

then D . 1 <= D2 . k by A37, A161, A162, SEQ_4:137;

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

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

proof

D2 . k in rng D2
by A151, FUNCT_1:def 3;
j1 in Seg (len (D1 | j1))
by A146, A152, FINSEQ_1:1;

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

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

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

j1 in Seg j1 by A146, FINSEQ_1:1;

hence D2 . k in rng (D1 | j1) by A41, A160, A165, A164, RFINSEQ:6; :: thesis: verum

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

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

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

j1 in Seg j1 by A146, FINSEQ_1:1;

hence D2 . k in rng (D1 | j1) by A41, A160, A165, A164, RFINSEQ:6; :: thesis: verum

hence x1 in rng (D1 | j1) by A11, A44, A149, A150, A163, A154, RFINSEQ:6, XBOOLE_0:def 3; :: thesis: verum

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

mid (D1,1,j1) is increasing by A38, A40, A146, INTEGRA1:7, INTEGRA1:35;

then A167: D1 | j1 is increasing by A146, FINSEQ_6:116;

then A168: D2 | (indx (D2,D1,j1)) = D1 | j1 by A47, A166, Th6;

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

k = indx (D2,D1,k)

proof

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

assume that

A170: 1 <= k and

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

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

end;assume that

A170: 1 <= k and

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

assume A172: 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 A172, XXREAL_0:1;

end;

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

k <= len D1
by A133, A171, XXREAL_0:2;

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

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

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

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

A176: indx (D2,D1,k) < j1 by A171, A173, XXREAL_0:2;

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

indx (D2,D1,k) <= indx (D2,D1,j1) by A10, A41, A171, A174, Th7;

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

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

indx (D2,D1,k) <= len D1 by A133, A176, XXREAL_0:2;

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

then A179: D1 . k > D1 . (indx (D2,D1,k)) by A173, A174, SEQM_3:def 1;

D1 . k = D2 . (indx (D2,D1,k)) by A10, A174, INTEGRA1:def 19;

hence contradiction by A41, A168, A178, A179, A177, RFINSEQ:6; :: thesis: verum

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

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

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

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

A176: indx (D2,D1,k) < j1 by A171, A173, XXREAL_0:2;

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

indx (D2,D1,k) <= indx (D2,D1,j1) by A10, A41, A171, A174, Th7;

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

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

indx (D2,D1,k) <= len D1 by A133, A176, XXREAL_0:2;

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

then A179: D1 . k > D1 . (indx (D2,D1,k)) by A173, A174, SEQM_3:def 1;

D1 . k = D2 . (indx (D2,D1,k)) by A10, A174, INTEGRA1:def 19;

hence contradiction by A41, A168, A178, A179, A177, RFINSEQ:6; :: thesis: verum

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

k <= len D1
by A133, A171, XXREAL_0:2;

then A181: k in dom D1 by A170, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A10, A41, A171, Th7;

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

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

then A183: k in dom D2 by A170, FINSEQ_3:25;

k in Seg j1 by A170, A171, FINSEQ_1:1;

then A184: D1 . k = (D1 | j1) . k by A43, RFINSEQ:6;

indx (D2,D1,k) in dom D2 by A10, A181, INTEGRA1:def 19;

then A185: D2 . k < D2 . (indx (D2,D1,k)) by A180, A183, SEQM_3:def 1;

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

D1 . k = D2 . (indx (D2,D1,k)) by A10, A181, INTEGRA1:def 19;

hence contradiction by A44, A168, A184, A185, A186, RFINSEQ:6; :: thesis: verum

end;then A181: k in dom D1 by A170, FINSEQ_3:25;

then indx (D2,D1,k) <= indx (D2,D1,j1) by A10, A41, A171, Th7;

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

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

then A183: k in dom D2 by A170, FINSEQ_3:25;

k in Seg j1 by A170, A171, FINSEQ_1:1;

then A184: D1 . k = (D1 | j1) . k by A43, RFINSEQ:6;

indx (D2,D1,k) in dom D2 by A10, A181, INTEGRA1:def 19;

then A185: D2 . k < D2 . (indx (D2,D1,k)) by A180, A183, SEQM_3:def 1;

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

D1 . k = D2 . (indx (D2,D1,k)) by A10, A181, INTEGRA1:def 19;

hence contradiction by A44, A168, A184, A185, A186, RFINSEQ:6; :: thesis: verum

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

proof

indx (D2,D1,j1) in dom D2
by A10, A43, INTEGRA1:def 19;
indx (D2,D1,j1) in Seg (len D2)
by A44, FINSEQ_1:def 3;

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

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

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

assume that

A189: 1 <= k and

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

A191: len (upper_volume (f,D1)) = len D1 by INTEGRA1:def 6;

then A192: k <= j1 by A133, A190, FINSEQ_1:59;

then A193: k in Seg j1 by A189, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A169, A189, A192;

then A194: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A146, A169;

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

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

k <= len D1 by A133, A192, XXREAL_0:2;

then A196: k in Seg (len D1) by A189, FINSEQ_1:1;

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

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

A199: D1 . k = D2 . (indx (D2,D1,k)) by A10, A197, INTEGRA1:def 19;

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

then A212: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A200, INTEGRA1:4;

A213: k in dom D1 by A196, FINSEQ_1:def 3;

j1 in Seg (len (upper_volume (f,D1))) by A41, A191, FINSEQ_1:def 3;

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

then A214: ((upper_volume (f,D1)) | j1) . k = (upper_volume (f,D1)) . k by A193, RFINSEQ:6

.= (upper_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A213, A212, INTEGRA1:def 6 ;

1 <= indx (D2,D1,k) by A169, A189, A192, A193;

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

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

((upper_volume (f,D2)) | (indx (D2,D1,j1))) . k = ((upper_volume (f,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A169, A189, A192, A193

.= (upper_volume (f,D2)) . (indx (D2,D1,k)) by A194, A188, RFINSEQ:6

.= (upper_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A215, INTEGRA1:def 6 ;

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

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

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

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

assume that

A189: 1 <= k and

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

A191: len (upper_volume (f,D1)) = len D1 by INTEGRA1:def 6;

then A192: k <= j1 by A133, A190, FINSEQ_1:59;

then A193: k in Seg j1 by A189, FINSEQ_1:1;

then indx (D2,D1,k) in Seg j1 by A169, A189, A192;

then A194: indx (D2,D1,k) in Seg (indx (D2,D1,j1)) by A146, A169;

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

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

k <= len D1 by A133, A192, XXREAL_0:2;

then A196: k in Seg (len D1) by A189, FINSEQ_1:1;

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

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

A199: D1 . k = D2 . (indx (D2,D1,k)) by A10, A197, INTEGRA1:def 19;

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

proof
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 A201:
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 A202:
upper_bound (divset (D1,k)) = D1 . k
by A197, INTEGRA1:def 4;

A203: lower_bound (divset (D1,k)) = lower_bound A by A197, A201, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A146, A169, A201;

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

end;A203: lower_bound (divset (D1,k)) = lower_bound A by A197, A201, INTEGRA1:def 4;

indx (D2,D1,k) = 1 by A146, A169, A201;

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

suppose A204:
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 A197, INTEGRA1:7;

k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A205: k1 <= j1 by A192, XXREAL_0:2;

A206: k - 1 in dom D1 by A197, A204, INTEGRA1:7;

then 1 <= k1 by FINSEQ_3:25;

then k1 = indx (D2,D1,k1) by A169, A205;

then A207: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A169, A189, A192, A193;

A208: indx (D2,D1,k) <> 1 by A169, A189, A192, A193, A204;

then A209: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A198, INTEGRA1:def 4;

A210: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A198, A208, INTEGRA1:def 4;

A211: upper_bound (divset (D1,k)) = D1 . k by A197, A204, INTEGRA1:def 4;

lower_bound (divset (D1,k)) = D1 . (k - 1) by A197, A204, 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 A10, A197, A211, A206, A209, A210, A207, INTEGRA1:def 19; :: thesis: verum

end;k <= k + 1 by NAT_1:11;

then k1 <= k by XREAL_1:20;

then A205: k1 <= j1 by A192, XXREAL_0:2;

A206: k - 1 in dom D1 by A197, A204, INTEGRA1:7;

then 1 <= k1 by FINSEQ_3:25;

then k1 = indx (D2,D1,k1) by A169, A205;

then A207: D2 . ((indx (D2,D1,k)) - 1) = D2 . (indx (D2,D1,k1)) by A169, A189, A192, A193;

A208: indx (D2,D1,k) <> 1 by A169, A189, A192, A193, A204;

then A209: lower_bound (divset (D2,(indx (D2,D1,k)))) = D2 . ((indx (D2,D1,k)) - 1) by A198, INTEGRA1:def 4;

A210: upper_bound (divset (D2,(indx (D2,D1,k)))) = D2 . (indx (D2,D1,k)) by A198, A208, INTEGRA1:def 4;

A211: upper_bound (divset (D1,k)) = D1 . k by A197, A204, INTEGRA1:def 4;

lower_bound (divset (D1,k)) = D1 . (k - 1) by A197, A204, 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 A10, A197, A211, A206, A209, A210, A207, INTEGRA1:def 19; :: thesis: verum

then A212: divset (D1,k) = divset (D2,(indx (D2,D1,k))) by A200, INTEGRA1:4;

A213: k in dom D1 by A196, FINSEQ_1:def 3;

j1 in Seg (len (upper_volume (f,D1))) by A41, A191, FINSEQ_1:def 3;

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

then A214: ((upper_volume (f,D1)) | j1) . k = (upper_volume (f,D1)) . k by A193, RFINSEQ:6

.= (upper_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A213, A212, INTEGRA1:def 6 ;

1 <= indx (D2,D1,k) by A169, A189, A192, A193;

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

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

((upper_volume (f,D2)) | (indx (D2,D1,j1))) . k = ((upper_volume (f,D2)) | (indx (D2,D1,j1))) . (indx (D2,D1,k)) by A169, A189, A192, A193

.= (upper_volume (f,D2)) . (indx (D2,D1,k)) by A194, A188, RFINSEQ:6

.= (upper_bound (rng (f | (divset (D2,(indx (D2,D1,k))))))) * (vol (divset (D2,(indx (D2,D1,k))))) by A215, INTEGRA1:def 6 ;

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

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

then A216: indx (D2,D1,j1) <= len (upper_volume (f,D2)) by INTEGRA1:def 6;

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

then A217: j1 <= len (upper_volume (f,D1)) by INTEGRA1:def 6;

len (D2 | (indx (D2,D1,j1))) = len (D1 | j1) by A47, A167, A166, Th6;

then indx (D2,D1,j1) = j1 by A133, A131, FINSEQ_1:59;

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

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

then A218: (upper_volume (f,D2)) | (indx (D2,D1,j1)) = (upper_volume (f,D1)) | j1 by A187, FINSEQ_1:14;

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

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

indx (D2,D1,j) in Seg (len H

then A221: indx (D2,D1,j) in dom H

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

then A222: indx (D2,D1,j) <= len H

j in Seg (len H

then A223: j in dom H

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

then A224: j <= len H

j1 in Seg (len D1) by A41, 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 A225: H

indx (D2,D1,j1) in Seg (len D2) by A44, 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 A226: H

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

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

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

then H

.= H

hence H

A227: 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] )

A228: i >= 1 by NAT_1:14;

assume A229: S_{1}[i]
; :: thesis: S_{1}[i + 1]

S_{1}[i + 1]

A228: i >= 1 by NAT_1:14;

assume A229: S

S

proof

A230:
i <= i + 1
by NAT_1:11;

assume A231: 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}(D1,j) - H_{2}(D2, indx (D2,D1,j)) <= ((i + 1) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )

then consider j being Element of NAT such that

A232: j in dom D1 and

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

A234: D2 . (indx (D2,D1,j)) = D1 . j by A10, A232, INTEGRA1:def 19;

i + 1 in Seg (len D) by A231, FINSEQ_1:def 3;

then i + 1 <= len D by FINSEQ_1:1;

then i <= len D by A230, XXREAL_0:2;

then A235: i in Seg (len D) by A228, FINSEQ_1:1;

then A236: i in dom D by FINSEQ_1:def 3;

A237: indx (D2,D1,j) in dom D2 by A10, A232, INTEGRA1:def 19;

then A238: 1 <= indx (D2,D1,j) by FINSEQ_3:25;

A239: indx (D2,D1,j) <= len D2 by A237, FINSEQ_3:25;

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

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}(D1,n1) - H_{2}(D2, indx (D2,D1,n1)) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)
by A229, A235, FINSEQ_1:def 3;

A244: 1 <= n1 + 1 by NAT_1:12;

A245: n1 < j

A259: 1 <= n1 by A241, FINSEQ_3:25;

A260: D2 . (indx (D2,D1,n1)) = D1 . n1 by A10, A241, INTEGRA1:def 19;

A261: 1 <= j by A232, FINSEQ_3:25;

A262: indx (D2,D1,n1) in dom D2 by A10, A241, INTEGRA1:def 19;

then A263: 1 <= indx (D2,D1,n1) by FINSEQ_3:25;

A264: j <= len D1 by A232, FINSEQ_3:25;

then A265: n1 + 1 <= len D1 by A258, XXREAL_0:2;

then A266: n1 + 1 in dom D1 by A244, FINSEQ_3:25;

then A267: D2 . (indx (D2,D1,(n1 + 1))) = D1 . (n1 + 1) by A10, INTEGRA1:def 19;

A268: j <= len H_{1}(D1)
by A264, INTEGRA1:def 6;

then j in Seg (len H_{1}(D1))
by A261, FINSEQ_1:1;

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

A270: indx (D2,D1,(n1 + 1)) in dom D2 by A10, A266, INTEGRA1:def 19;

then A271: 1 <= indx (D2,D1,(n1 + 1)) by 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 6;

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 A259, 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, A259, A268, INTEGRA2:4

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

then A272: H_{2}(D1,j) = H_{2}(D1,n1) + (Sum (mid (H_{1}(D1),(n1 + 1),j)))
by A269, INTEGRA1:def 20;

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

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

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

A274: indx (D2,D1,(n1 + 1)) <= len D2 by A270, FINSEQ_3:25;

D1 . (n1 + 1) <= D1 . j by A232, A258, A266, SEQ_4:137;

then A275: indx (D2,D1,(n1 + 1)) <= indx (D2,D1,j) by A270, A267, A237, A234, SEQM_3:def 1;

then 1 + (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) + 1 by XREAL_1:6;

then 1 <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;

then A276: (mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j)))) . 1 = D2 . ((1 - 1) + (indx (D2,D1,(n1 + 1)))) by A275, A271, A239, FINSEQ_6:122

.= D1 . (n1 + 1) by A10, A266, INTEGRA1:def 19 ;

A277: n1 >= 1 by A241, FINSEQ_3:25;

A278: j - n1 >= 1 by A258, XREAL_1:19;

(Sum (mid (H_{1}(D1),(n1 + 1),j))) - (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

assume A231: 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

A232: j in dom D1 and

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

A234: D2 . (indx (D2,D1,j)) = D1 . j by A10, A232, INTEGRA1:def 19;

i + 1 in Seg (len D) by A231, FINSEQ_1:def 3;

then i + 1 <= len D by FINSEQ_1:1;

then i <= len D by A230, XXREAL_0:2;

then A235: i in Seg (len D) by A228, FINSEQ_1:1;

then A236: i in dom D by FINSEQ_1:def 3;

A237: indx (D2,D1,j) in dom D2 by A10, A232, INTEGRA1:def 19;

then A238: 1 <= indx (D2,D1,j) by FINSEQ_3:25;

A239: indx (D2,D1,j) <= len D2 by A237, FINSEQ_3:25;

then A240: indx (D2,D1,j) <= len H

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 A258:
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 A236, 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 A231, FUNCT_1:def 3;

then A249: D . (i + 1) in (rng D) /\ (divset (D1,j)) by A233, XBOOLE_0:def 4;

i + 1 > i by XREAL_1:29;

hence contradiction by A8, A231, A232, A236, 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 A231, FUNCT_1:def 3;

then A249: D . (i + 1) in (rng D) /\ (divset (D1,j)) by A233, XBOOLE_0:def 4;

i + 1 > i by XREAL_1:29;

hence contradiction by A8, A231, A232, A236, 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 A232, FINSEQ_3:25;

then 1 + 1 <= j + 1 by XREAL_1:6;

then A252: n1 <> 1 by A250, XXREAL_0:2;

then n1 - 1 in dom D1 by A241, INTEGRA1:7;

then A253: D1 . j <= D1 . (n1 - 1) by A232, A251, SEQ_4:137;

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

lower_bound (divset (D1,n1)) = D1 . (n1 - 1) by A241, A252, INTEGRA1:def 4;

then A256: D . i >= D1 . j by A255, A253, XXREAL_0:2;

A257: i < i + 1 by XREAL_1:29;

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

then D . i >= D . (i + 1) by A254, A256, XXREAL_0:2;

hence contradiction by A231, A236, A257, SEQM_3:def 1; :: thesis: verum

end;then A251: n1 - 1 >= j by XREAL_1:19;

1 <= j by A232, FINSEQ_3:25;

then 1 + 1 <= j + 1 by XREAL_1:6;

then A252: n1 <> 1 by A250, XXREAL_0:2;

then n1 - 1 in dom D1 by A241, INTEGRA1:7;

then A253: D1 . j <= D1 . (n1 - 1) by A232, A251, SEQ_4:137;

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

proof
end;

A255:
lower_bound (divset (D1,n1)) <= D . i
by A242, INTEGRA2:1;lower_bound (divset (D1,n1)) = D1 . (n1 - 1) by A241, A252, INTEGRA1:def 4;

then A256: D . i >= D1 . j by A255, A253, XXREAL_0:2;

A257: i < i + 1 by XREAL_1:29;

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

then D . i >= D . (i + 1) by A254, A256, XXREAL_0:2;

hence contradiction by A231, A236, A257, SEQM_3:def 1; :: thesis: verum

A259: 1 <= n1 by A241, FINSEQ_3:25;

A260: D2 . (indx (D2,D1,n1)) = D1 . n1 by A10, A241, INTEGRA1:def 19;

A261: 1 <= j by A232, FINSEQ_3:25;

A262: indx (D2,D1,n1) in dom D2 by A10, A241, INTEGRA1:def 19;

then A263: 1 <= indx (D2,D1,n1) by FINSEQ_3:25;

A264: j <= len D1 by A232, FINSEQ_3:25;

then A265: n1 + 1 <= len D1 by A258, XXREAL_0:2;

then A266: n1 + 1 in dom D1 by A244, FINSEQ_3:25;

then A267: D2 . (indx (D2,D1,(n1 + 1))) = D1 . (n1 + 1) by A10, INTEGRA1:def 19;

A268: j <= len H

then j in Seg (len H

then A269: j in dom H

A270: indx (D2,D1,(n1 + 1)) in dom D2 by A10, A266, INTEGRA1:def 19;

then A271: 1 <= indx (D2,D1,(n1 + 1)) by 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 A272: H

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

then indx (D2,D1,j) in Seg (len H

then A273: indx (D2,D1,j) in dom H

A274: indx (D2,D1,(n1 + 1)) <= len D2 by A270, FINSEQ_3:25;

D1 . (n1 + 1) <= D1 . j by A232, A258, A266, SEQ_4:137;

then A275: indx (D2,D1,(n1 + 1)) <= indx (D2,D1,j) by A270, A267, A237, A234, SEQM_3:def 1;

then 1 + (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) + 1 by XREAL_1:6;

then 1 <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;

then A276: (mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j)))) . 1 = D2 . ((1 - 1) + (indx (D2,D1,(n1 + 1)))) by A275, A271, A239, FINSEQ_6:122

.= D1 . (n1 + 1) by A10, A266, INTEGRA1:def 19 ;

A277: n1 >= 1 by A241, FINSEQ_3:25;

A278: j - n1 >= 1 by A258, XREAL_1:19;

(Sum (mid (H

proof

per cases
( n1 + 1 = j or n1 + 1 < j )
by A258, XXREAL_0:1;

suppose A279:
n1 + 1 = j
; :: thesis: (Sum (mid (H_{1}(D1),(n1 + 1),j))) - (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

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

A310: indx (D2,D1,j) <= len H_{1}(D2)
by A239, INTEGRA1:def 6;

D1 . n1 < D1 . j by A232, A241, A245, SEQM_3:def 1;

then A311: indx (D2,D1,n1) < indx (D2,D1,j) by A262, A260, A237, A234, SEQ_4:137;

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

then (indx (D2,D1,n1)) + 1 <= len D2 by A239, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len H_{1}(D2)
by INTEGRA1:def 6;

then A313: 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 A238, A312, A309, A310, FINSEQ_6:118

.= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A312, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,n1)) ;

(indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A311, NAT_1:13;

then A314: ( (indx (D2,D1,n1)) + 1 = indx (D2,D1,j) or (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ) by XXREAL_0:1;

A315: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
_{1}(D1)
by A265, INTEGRA1:def 6;

(j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A279, XREAL_1:233;

then A342: len (mid (H_{1}(D1),(n1 + 1),j)) = 1
by A244, A279, A341, FINSEQ_6:118;

reconsider uv = (upper_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 A258, 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 + (n1 + 1)) - 1)
by A244, A279, A341, FINSEQ_6:122

.= (upper_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) by A266, INTEGRA1:def 6 ;

then mid (H_{1}(D1),(n1 + 1),j) = <*uv*>
by A342, FINSEQ_1:40;

then A343: Sum (mid (H_{1}(D1),(n1 + 1),j)) = (upper_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1))))
by FINSOP_1:11;

divset (D1,(n1 + 1)) c= A by A266, INTEGRA1:8;

then A344: upper_bound (rng (f | (divset (D1,(n1 + 1))))) <= upper_bound (rng f) by A1, Lm4;

n1 + 1 in Seg (len D1) by A266, FINSEQ_1:def 3;

then n1 + 1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;

then A345: n1 + 1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;

vol (divset (D1,(n1 + 1))) = (upper_volume ((chi (A,A)),D1)) . (n1 + 1) by A266, INTEGRA1:20;

then vol (divset (D1,(n1 + 1))) in rng (upper_volume ((chi (A,A)),D1)) by A345, FUNCT_1:def 3;

then A346: 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 A347: ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,(n1 + 1)))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A346, XREAL_1:64;

vol (divset (D1,(n1 + 1))) >= 0 by INTEGRA1:9;

then Sum (mid (H_{1}(D1),(n1 + 1),j)) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A343, A344, XREAL_1:64;

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

hence (Sum (mid (H_{1}(D1),(n1 + 1),j))) - (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
by A347, XXREAL_0:2; :: thesis: verum

end;proof

A307:
( (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) implies (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) )
A281:
upper_bound (divset (D1,j)) = D1 . j
by A232, A245, A277, INTEGRA1:def 4;

A282: lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 4;

A283: 1 <= (indx (D2,D1,n1)) + 1 by A263, NAT_1:13;

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

then A284: (indx (D2,D1,n1)) + 2 < indx (D2,D1,j) by XREAL_1:20;

then A285: (indx (D2,D1,n1)) + 2 <= len D2 by A239, XXREAL_0:2;

A286: (indx (D2,D1,n1)) + 1 < (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then A287: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 2 by NAT_1:13;

then 1 <= (indx (D2,D1,n1)) + 2 by A263, XXREAL_0:2;

then A288: (indx (D2,D1,n1)) + 2 in dom D2 by A285, FINSEQ_3:25;

then A289: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 2) by A237, A284, SEQ_4:137;

A290: not D2 . ((indx (D2,D1,n1)) + 2) in rng D1

then A294: D2 . ((indx (D2,D1,n1)) + 2) in rng D by A11, A290, XBOOLE_0:def 3;

A295: lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 4;

A296: upper_bound (divset (D1,j)) = D1 . j by A232, A245, A277, INTEGRA1:def 4;

D2 . ((indx (D2,D1,n1)) + 2) >= D2 . (indx (D2,D1,n1)) by A262, A287, A288, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 2) in divset (D1,j) by A260, A234, A279, A295, A281, A289, INTEGRA2:1;

then A297: D2 . ((indx (D2,D1,n1)) + 2) in (rng D) /\ (divset (D1,j)) by A294, XBOOLE_0:def 4;

A298: (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) by A284, A286, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len D2 by A239, XXREAL_0:2;

then A299: (indx (D2,D1,n1)) + 1 in dom D2 by A283, FINSEQ_3:25;

then A300: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 1) by A237, A298, SEQ_4:137;

A301: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A302: not D2 . ((indx (D2,D1,n1)) + 1) in rng D1

then A306: D2 . ((indx (D2,D1,n1)) + 1) in rng D by A11, A302, XBOOLE_0:def 3;

D2 . ((indx (D2,D1,n1)) + 1) >= D2 . (indx (D2,D1,n1)) by A262, A301, A299, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 1) in divset (D1,j) by A260, A234, A279, A282, A296, A300, INTEGRA2:1;

then D2 . ((indx (D2,D1,n1)) + 1) in (rng D) /\ (divset (D1,j)) by A306, XBOOLE_0:def 4;

then D2 . ((indx (D2,D1,n1)) + 1) = D2 . ((indx (D2,D1,n1)) + 2) by A8, A232, A297, Th5;

hence contradiction by A286, A299, A288, SEQM_3:def 1; :: thesis: verum

end;A282: lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 4;

A283: 1 <= (indx (D2,D1,n1)) + 1 by A263, NAT_1:13;

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

then A284: (indx (D2,D1,n1)) + 2 < indx (D2,D1,j) by XREAL_1:20;

then A285: (indx (D2,D1,n1)) + 2 <= len D2 by A239, XXREAL_0:2;

A286: (indx (D2,D1,n1)) + 1 < (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then A287: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 2 by NAT_1:13;

then 1 <= (indx (D2,D1,n1)) + 2 by A263, XXREAL_0:2;

then A288: (indx (D2,D1,n1)) + 2 in dom D2 by A285, FINSEQ_3:25;

then A289: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 2) by A237, A284, SEQ_4:137;

A290: not D2 . ((indx (D2,D1,n1)) + 2) in rng D1

proof

D2 . ((indx (D2,D1,n1)) + 2) in rng D2
by A288, 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

A291: k1 in dom D1 and

A292: D2 . ((indx (D2,D1,n1)) + 2) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 2) < D2 . (indx (D2,D1,j)) by A237, A284, A288, SEQM_3:def 1;

then A293: k1 < j by A232, A234, A291, A292, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 2) by A262, A287, A288, SEQM_3:def 1;

then n1 < k1 by A241, A260, A291, A292, SEQ_4:137;

hence contradiction by A279, A293, NAT_1:13; :: thesis: verum

end;then consider k1 being Element of NAT such that

A291: k1 in dom D1 and

A292: D2 . ((indx (D2,D1,n1)) + 2) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 2) < D2 . (indx (D2,D1,j)) by A237, A284, A288, SEQM_3:def 1;

then A293: k1 < j by A232, A234, A291, A292, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 2) by A262, A287, A288, SEQM_3:def 1;

then n1 < k1 by A241, A260, A291, A292, SEQ_4:137;

hence contradiction by A279, A293, NAT_1:13; :: thesis: verum

then A294: D2 . ((indx (D2,D1,n1)) + 2) in rng D by A11, A290, XBOOLE_0:def 3;

A295: lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 4;

A296: upper_bound (divset (D1,j)) = D1 . j by A232, A245, A277, INTEGRA1:def 4;

D2 . ((indx (D2,D1,n1)) + 2) >= D2 . (indx (D2,D1,n1)) by A262, A287, A288, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 2) in divset (D1,j) by A260, A234, A279, A295, A281, A289, INTEGRA2:1;

then A297: D2 . ((indx (D2,D1,n1)) + 2) in (rng D) /\ (divset (D1,j)) by A294, XBOOLE_0:def 4;

A298: (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) by A284, A286, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len D2 by A239, XXREAL_0:2;

then A299: (indx (D2,D1,n1)) + 1 in dom D2 by A283, FINSEQ_3:25;

then A300: D2 . (indx (D2,D1,j)) >= D2 . ((indx (D2,D1,n1)) + 1) by A237, A298, SEQ_4:137;

A301: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A302: not D2 . ((indx (D2,D1,n1)) + 1) in rng D1

proof

D2 . ((indx (D2,D1,n1)) + 1) in rng D2
by A299, 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

A303: k1 in dom D1 and

A304: D2 . ((indx (D2,D1,n1)) + 1) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 1) < D2 . (indx (D2,D1,j)) by A237, A298, A299, SEQM_3:def 1;

then A305: k1 < j by A232, A234, A303, A304, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A262, A301, A299, SEQM_3:def 1;

then n1 < k1 by A241, A260, A303, A304, SEQ_4:137;

hence contradiction by A279, A305, NAT_1:13; :: thesis: verum

end;then consider k1 being Element of NAT such that

A303: k1 in dom D1 and

A304: D2 . ((indx (D2,D1,n1)) + 1) = D1 . k1 by PARTFUN1:3;

D2 . ((indx (D2,D1,n1)) + 1) < D2 . (indx (D2,D1,j)) by A237, A298, A299, SEQM_3:def 1;

then A305: k1 < j by A232, A234, A303, A304, SEQ_4:137;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A262, A301, A299, SEQM_3:def 1;

then n1 < k1 by A241, A260, A303, A304, SEQ_4:137;

hence contradiction by A279, A305, NAT_1:13; :: thesis: verum

then A306: D2 . ((indx (D2,D1,n1)) + 1) in rng D by A11, A302, XBOOLE_0:def 3;

D2 . ((indx (D2,D1,n1)) + 1) >= D2 . (indx (D2,D1,n1)) by A262, A301, A299, SEQ_4:137;

then D2 . ((indx (D2,D1,n1)) + 1) in divset (D1,j) by A260, A234, A279, A282, A296, A300, INTEGRA2:1;

then D2 . ((indx (D2,D1,n1)) + 1) in (rng D) /\ (divset (D1,j)) by A306, XBOOLE_0:def 4;

then D2 . ((indx (D2,D1,n1)) + 1) = D2 . ((indx (D2,D1,n1)) + 2) by A8, A232, A297, Th5;

hence contradiction by A286, A299, A288, SEQM_3:def 1; :: thesis: verum

proof

A309:
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 A308: ((indx (D2,D1,n1)) + 1) + 1 <= indx (D2,D1,j) by NAT_1:13;

(indx (D2,D1,n1)) + 2 >= indx (D2,D1,j) by A280, XREAL_1:20;

hence (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) by A308, XXREAL_0:1; :: thesis: verum

end;then A308: ((indx (D2,D1,n1)) + 1) + 1 <= indx (D2,D1,j) by NAT_1:13;

(indx (D2,D1,n1)) + 2 >= indx (D2,D1,j) by A280, XREAL_1:20;

hence (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) by A308, XXREAL_0:1; :: thesis: verum

A310: indx (D2,D1,j) <= len H

D1 . n1 < D1 . j by A232, A241, A245, SEQM_3:def 1;

then A311: indx (D2,D1,n1) < indx (D2,D1,j) by A262, A260, A237, A234, SEQ_4:137;

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

then (indx (D2,D1,n1)) + 1 <= len D2 by A239, XXREAL_0:2;

then (indx (D2,D1,n1)) + 1 <= len H

then A313: len (mid (H

.= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A312, XREAL_1:233

.= (indx (D2,D1,j)) - (indx (D2,D1,n1)) ;

(indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A311, NAT_1:13;

then A314: ( (indx (D2,D1,n1)) + 1 = indx (D2,D1,j) or (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ) by XXREAL_0:1;

A315: Sum (mid (H

proof
_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
; :: thesis: verum

end;

A341:
n1 + 1 <= len Hnow :: thesis: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))end;

hence
Sum (mid (Hper cases
( (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1 or (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2 )
by A314, A307;

end;

suppose A316:
(indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1
; :: thesis: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))

(indx (D2,D1,n1)) + 1 >= 1 + 1
by A263, XREAL_1:6;

then A317: (indx (D2,D1,n1)) + 1 <> 1 ;

then upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A237, A316, INTEGRA1:def 4;

then A318: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . j by A10, A232, A316, INTEGRA1:def 19;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A237, A316, A317, INTEGRA1:def 4;

then A319: lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . n1 by A10, A241, INTEGRA1:def 19;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A277, A266, A279, INTEGRA1:def 4;

then A320: divset (D2,((indx (D2,D1,n1)) + 1)) = divset (D1,(n1 + 1)) by A245, A277, A266, A279, A319, A318, INTEGRA1:def 4;

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

reconsider UV = 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 A316;

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 A309, A310, FINSEQ_6:122

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

then A322: mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*UV*>
by A313, A316, FINSEQ_1:40;

H_{1}(D2) . ((indx (D2,D1,n1)) + 1) = (upper_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))
by A237, A316, INTEGRA1:def 6;

then H_{1}(D2) . ((indx (D2,D1,n1)) + 1) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A1, A237, A316, A320, A321, Th19, XREAL_1:64;

hence Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A322, FINSOP_1:11; :: thesis: verum

end;then A317: (indx (D2,D1,n1)) + 1 <> 1 ;

then upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A237, A316, INTEGRA1:def 4;

then A318: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . j by A10, A232, A316, INTEGRA1:def 19;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A237, A316, A317, INTEGRA1:def 4;

then A319: lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D1 . n1 by A10, A241, INTEGRA1:def 19;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A277, A266, A279, INTEGRA1:def 4;

then A320: divset (D2,((indx (D2,D1,n1)) + 1)) = divset (D1,(n1 + 1)) by A245, A277, A266, A279, A319, A318, INTEGRA1:def 4;

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

reconsider UV = H

1 = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A316;

then (mid (H

.= H

then A322: mid (H

H

then H

hence Sum (mid (H

suppose A323:
(indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2
; :: thesis: Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))

(indx (D2,D1,n1)) + 2 >= 2 + 1
by A263, XREAL_1:6;

then A324: (indx (D2,D1,n1)) + 2 <> 1 ;

then A325: upper_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . (indx (D2,D1,j)) by A237, A323, INTEGRA1:def 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 A237, A323, A324, INTEGRA1:def 4;

then A326: vol (divset (D2,((indx (D2,D1,n1)) + 2))) = (D1 . j) - (D2 . ((indx (D2,D1,n1)) + 1)) by A234, A325, INTEGRA1:def 5;

A327: upper_bound (divset (D1,(n1 + 1))) = D1 . (n1 + 1) by A245, A277, A266, A279, INTEGRA1:def 4;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A277, A266, A279, INTEGRA1:def 4;

then A328: vol (divset (D1,(n1 + 1))) = (D1 . (n1 + 1)) - (D1 . n1) by A327, INTEGRA1:def 5;

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

A330: indx (D2,D1,j) <= len H_{1}(D2)
by A239, INTEGRA1:def 6;

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

A332: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;

A333: (indx (D2,D1,n1)) + 1 <= (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then (indx (D2,D1,n1)) + 1 <= len D2 by A239, A323, XXREAL_0:2;

then A334: (indx (D2,D1,n1)) + 1 in dom D2 by A332, FINSEQ_3:25;

then H_{1}(D2) . ((indx (D2,D1,n1)) + 1) = (upper_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 1)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))
by INTEGRA1:def 6;

then A335: H_{1}(D2) . ((indx (D2,D1,n1)) + 1) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 1))))
by A1, A334, A331, Th19, XREAL_1:64;

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 = 1 + 1 by A323;

then A336: (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 A332, A333, A330, FINSEQ_6:122

.= H_{1}(D2) . (((indx (D2,D1,n1)) + 0) + 2)
;

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 >= 1 by A323;

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 A323, A332, A333, A330, 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 A313, A323, A336, FINSEQ_1:44;

then A337: 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;

A338: (indx (D2,D1,n1)) + 1 > 1 by A263, NAT_1:13;

then A339: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A334, INTEGRA1:def 4;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A334, A338, INTEGRA1:def 4;

then A340: vol (divset (D2,((indx (D2,D1,n1)) + 1))) = (D2 . ((indx (D2,D1,n1)) + 1)) - (D1 . n1) by A260, A339, INTEGRA1:def 5;

H_{1}(D2) . ((indx (D2,D1,n1)) + 2) = (upper_bound (rng (f | (divset (D2,((indx (D2,D1,n1)) + 2)))))) * (vol (divset (D2,((indx (D2,D1,n1)) + 2))))
by A237, A323, INTEGRA1:def 6;

then H_{1}(D2) . ((indx (D2,D1,n1)) + 2) >= (lower_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,n1)) + 2))))
by A1, A237, A323, A329, Th19, XREAL_1:64;

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

hence Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
by A279, A340, A326, A328; :: thesis: verum

end;then A324: (indx (D2,D1,n1)) + 2 <> 1 ;

then A325: upper_bound (divset (D2,((indx (D2,D1,n1)) + 2))) = D2 . (indx (D2,D1,j)) by A237, A323, INTEGRA1:def 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 A237, A323, A324, INTEGRA1:def 4;

then A326: vol (divset (D2,((indx (D2,D1,n1)) + 2))) = (D1 . j) - (D2 . ((indx (D2,D1,n1)) + 1)) by A234, A325, INTEGRA1:def 5;

A327: upper_bound (divset (D1,(n1 + 1))) = D1 . (n1 + 1) by A245, A277, A266, A279, INTEGRA1:def 4;

lower_bound (divset (D1,(n1 + 1))) = D1 . ((n1 + 1) - 1) by A245, A277, A266, A279, INTEGRA1:def 4;

then A328: vol (divset (D1,(n1 + 1))) = (D1 . (n1 + 1)) - (D1 . n1) by A327, INTEGRA1:def 5;

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

A330: indx (D2,D1,j) <= len H

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

A332: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;

A333: (indx (D2,D1,n1)) + 1 <= (indx (D2,D1,n1)) + 2 by XREAL_1:6;

then (indx (D2,D1,n1)) + 1 <= len D2 by A239, A323, XXREAL_0:2;

then A334: (indx (D2,D1,n1)) + 1 in dom D2 by A332, FINSEQ_3:25;

then H

then A335: H

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 = 1 + 1 by A323;

then A336: (mid (H

.= H

((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 >= 1 by A323;

then (mid (H

.= H

then mid (H

then A337: Sum (mid (H

A338: (indx (D2,D1,n1)) + 1 > 1 by A263, NAT_1:13;

then A339: upper_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . ((indx (D2,D1,n1)) + 1) by A334, INTEGRA1:def 4;

lower_bound (divset (D2,((indx (D2,D1,n1)) + 1))) = D2 . (((indx (D2,D1,n1)) + 1) - 1) by A334, A338, INTEGRA1:def 4;

then A340: vol (divset (D2,((indx (D2,D1,n1)) + 1))) = (D2 . ((indx (D2,D1,n1)) + 1)) - (D1 . n1) by A260, A339, INTEGRA1:def 5;

H

then H

then Sum (mid (H

hence Sum (mid (H

(j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A279, XREAL_1:233;

then A342: len (mid (H

reconsider uv = (upper_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 A258, XREAL_1:6;

then 1 <= (j + 1) - (n1 + 1) by XREAL_1:19;

then (mid (H

.= (upper_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))) by A266, INTEGRA1:def 6 ;

then mid (H

then A343: Sum (mid (H

divset (D1,(n1 + 1)) c= A by A266, INTEGRA1:8;

then A344: upper_bound (rng (f | (divset (D1,(n1 + 1))))) <= upper_bound (rng f) by A1, Lm4;

n1 + 1 in Seg (len D1) by A266, FINSEQ_1:def 3;

then n1 + 1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;

then A345: n1 + 1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;

vol (divset (D1,(n1 + 1))) = (upper_volume ((chi (A,A)),D1)) . (n1 + 1) by A266, INTEGRA1:20;

then vol (divset (D1,(n1 + 1))) in rng (upper_volume ((chi (A,A)),D1)) by A345, FUNCT_1:def 3;

then A346: 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 A347: ((upper_bound (rng f)) - (lower_bound (rng f))) * (vol (divset (D1,(n1 + 1)))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A346, 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 A348:
n1 + 1 < j
; :: thesis: (Sum (mid (H_{1}(D1),(n1 + 1),j))) - (Sum (mid (H_{1}(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)

A349:
j -' (n1 + 1) = j - (n1 + 1)
by A258, XREAL_1:233;

then A350: (j -' (n1 + 1)) + 1 = j - n1 ;

A351: n1 < n1 + 1 by NAT_1:13;

then A352: D1 . n1 < D1 . (n1 + 1) by A241, A266, SEQM_3:def 1;

then consider B being non empty closed_interval Subset of REAL, MD1, MD2 being Division of B such that

A353: D1 . n1 = lower_bound B and

upper_bound B = MD2 . (len MD2) and

A354: upper_bound B = MD1 . (len MD1) and

A355: MD1 <= MD2 and

A356: MD1 = mid (D1,(n1 + 1),j) and

A357: MD2 = mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j))) by A10, A232, A258, A266, A276, Th15;

A358: len MD1 = (j -' (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A356, FINSEQ_6:118;

then A359: len MD1 = (j - (n1 + 1)) + 1 by A258, XREAL_1:233;

then A360: ((len MD1) + (n1 + 1)) - 1 = j ;

A361: len MD1 in dom MD1 by FINSEQ_5:6;

then A362: 1 <= len MD1 by FINSEQ_3:25;

A363: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

A379: delta MD1 >= 0 by Th9;

A380: g | B is bounded

then A388: D1 . (j - 1) <= D . (i + 1) by A232, A245, A277, INTEGRA1:def 4;

A389: (j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A258, XREAL_1:233;

A390: len (upper_volume (g,MD1)) = len MD1 by INTEGRA1:def 6

.= (j - (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A356, A389, FINSEQ_6:118 ;

A391: j <= len H_{1}(D1)
by A264, INTEGRA1:def 6;

A392: for k being Nat st 1 <= k & k <= len (upper_volume (g,MD1)) holds

(upper_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k
_{1}(D1)
by A265, INTEGRA1:def 6;

then len (upper_volume (g,MD1)) = len (mid (H_{1}(D1),(n1 + 1),j))
by A258, A261, A244, A389, A390, A391, FINSEQ_6:118;

then A415: Sum (upper_volume (g,MD1)) = Sum (mid (H_{1}(D1),(n1 + 1),j))
by A392, FINSEQ_1:14;

A416: n1 < j - 1 by A348, XREAL_1:20;

A417: 1 <= (indx (D2,D1,n1)) + 1 by A263, NAT_1:13;

A418: len MD1 in dom MD1 by FINSEQ_5:6;

A419: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

then vol B = (D1 . j) - (D1 . n1) by A232, A245, A277, A354, A363, A419, INTEGRA1:def 4;

then A420: vol B <> 0 by A232, A241, A245, SEQM_3:def 1;

rng f is bounded_below by A1, INTEGRA1:11;

then A421: 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 A421, XREAL_1:13;

then A422: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A379, XREAL_1:64;

D1 . n1 < D1 . (n1 + 1) by A241, A266, A351, SEQM_3:def 1;

then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A262, A260, A270, A267, SEQ_4:137;

then A423: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,(n1 + 1)) by NAT_1:13;

then A424: (indx (D2,D1,n1)) + 1 <= len D2 by A274, XXREAL_0:2;

A425: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A426: indx (D2,D1,(n1 + 1)) = (indx (D2,D1,n1)) + 1

then A444: len MD2 = ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by A275, XREAL_1:233;

then A445: len (upper_volume (g,MD2)) = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A426, INTEGRA1:def 6;

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

x1 in rng MD2

then A350: (j -' (n1 + 1)) + 1 = j - n1 ;

A351: n1 < n1 + 1 by NAT_1:13;

then A352: D1 . n1 < D1 . (n1 + 1) by A241, A266, SEQM_3:def 1;

then consider B being non empty closed_interval Subset of REAL, MD1, MD2 being Division of B such that

A353: D1 . n1 = lower_bound B and

upper_bound B = MD2 . (len MD2) and

A354: upper_bound B = MD1 . (len MD1) and

A355: MD1 <= MD2 and

A356: MD1 = mid (D1,(n1 + 1),j) and

A357: MD2 = mid (D2,(indx (D2,D1,(n1 + 1))),(indx (D2,D1,j))) by A10, A232, A258, A266, A276, Th15;

A358: len MD1 = (j -' (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A356, FINSEQ_6:118;

then A359: len MD1 = (j - (n1 + 1)) + 1 by A258, XREAL_1:233;

then A360: ((len MD1) + (n1 + 1)) - 1 = j ;

A361: len MD1 in dom MD1 by FINSEQ_5:6;

then A362: 1 <= len MD1 by FINSEQ_3:25;

A363: ( lower_bound (divset (MD1,(len MD1))) = lower_bound (divset (D1,j)) & upper_bound (divset (MD1,(len MD1))) = upper_bound (divset (D1,j)) )

proof
end;

A372:
B c= A
per cases
( len MD1 = 1 or len MD1 <> 1 )
;

end;

suppose A364:
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 A365:
upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)
by A361, INTEGRA1:def 4;

A366: upper_bound (divset (D1,j)) = D1 . j by A232, A245, A277, INTEGRA1:def 4;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, 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 A261, A264, A353, A356, A359, A361, A364, A365, A366, FINSEQ_6:118, INTEGRA1:def 4; :: thesis: verum

end;A366: upper_bound (divset (D1,j)) = D1 . j by A232, A245, A277, INTEGRA1:def 4;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, 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 A261, A264, A353, A356, A359, A361, A364, A365, A366, FINSEQ_6:118, INTEGRA1:def 4; :: thesis: verum

suppose A367:
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 A361, INTEGRA1:7;

then A368: (len MD1) - 1 >= 1 by FINSEQ_3:25;

len MD1 <= (len MD1) + 1 by NAT_1:11;

then A369: (len MD1) - 1 <= len MD1 by XREAL_1:20;

upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A361, A367, INTEGRA1:def 4;

then A370: upper_bound (divset (MD1,(len MD1))) = D1 . j by A258, A264, A244, A356, A358, A360, A362, FINSEQ_6:122;

A371: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A358, A349;

lower_bound (divset (MD1,(len MD1))) = MD1 . ((len MD1) - 1) by A361, A367, INTEGRA1:def 4;

then lower_bound (divset (MD1,(len MD1))) = D1 . (j - 1) by A258, A264, A244, A356, A358, A371, A368, A369, 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 A232, A245, A277, A370, INTEGRA1:def 4; :: thesis: verum

end;then A368: (len MD1) - 1 >= 1 by FINSEQ_3:25;

len MD1 <= (len MD1) + 1 by NAT_1:11;

then A369: (len MD1) - 1 <= len MD1 by XREAL_1:20;

upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1) by A361, A367, INTEGRA1:def 4;

then A370: upper_bound (divset (MD1,(len MD1))) = D1 . j by A258, A264, A244, A356, A358, A360, A362, FINSEQ_6:122;

A371: (((len MD1) - 1) + (n1 + 1)) - 1 = j - 1 by A358, A349;

lower_bound (divset (MD1,(len MD1))) = MD1 . ((len MD1) - 1) by A361, A367, INTEGRA1:def 4;

then lower_bound (divset (MD1,(len MD1))) = D1 . (j - 1) by A258, A264, A244, A356, A358, A371, A368, A369, 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 A232, A245, A277, A370, INTEGRA1:def 4; :: thesis: verum

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 )

A373: rng D1 c= A by INTEGRA1:def 2;

D1 . n1 in rng D1 by A241, FUNCT_1:def 3;

then A374: lower_bound A <= D1 . n1 by A373, INTEGRA2:1;

assume A375: x1 in B ; :: thesis: x1 in A

then reconsider x1 = x1 as Real ;

A376: x1 <= MD1 . (len MD1) by A354, A375, INTEGRA2:1;

D1 . j in rng D1 by A232, FUNCT_1:def 3;

then A377: D1 . j <= upper_bound A by A373, INTEGRA2:1;

D1 . n1 <= x1 by A353, A375, INTEGRA2:1;

then A378: lower_bound A <= x1 by A374, XXREAL_0:2;

MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A258, A278, A264, A244, A356, A358, A349, FINSEQ_6:122

.= D1 . j ;

then x1 <= upper_bound A by A376, A377, XXREAL_0:2;

hence x1 in A by A378, INTEGRA2:1; :: thesis: verum

end;A373: rng D1 c= A by INTEGRA1:def 2;

D1 . n1 in rng D1 by A241, FUNCT_1:def 3;

then A374: lower_bound A <= D1 . n1 by A373, INTEGRA2:1;

assume A375: x1 in B ; :: thesis: x1 in A

then reconsider x1 = x1 as Real ;

A376: x1 <= MD1 . (len MD1) by A354, A375, INTEGRA2:1;

D1 . j in rng D1 by A232, FUNCT_1:def 3;

then A377: D1 . j <= upper_bound A by A373, INTEGRA2:1;

D1 . n1 <= x1 by A353, A375, INTEGRA2:1;

then A378: lower_bound A <= x1 by A374, XXREAL_0:2;

MD1 . (len MD1) = D1 . (((j - n1) - 1) + (n1 + 1)) by A258, A278, A264, A244, A356, A358, A349, FINSEQ_6:122

.= D1 . j ;

then x1 <= upper_bound A by A376, A377, XXREAL_0:2;

hence x1 in A by A378, INTEGRA2:1; :: thesis: verum

A379: delta MD1 >= 0 by Th9;

A380: g | B is bounded

proof

lower_bound (divset (D1,j)) <= D . (i + 1)
by A233, INTEGRA2:1;
consider a being Real such that

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

A385: 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 A384; :: thesis: verum

end;A381: 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 A384:
g | B is bounded_below
by RFUNCT_1:71;
let x be object ; :: thesis: ( x in B /\ (dom g) implies a <= g . x )

A382: (dom f) /\ B c= (dom f) /\ A by A372, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: a <= g . x

then A383: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a <= f . x by A381, A382;

hence a <= g . x by A383, FUNCT_1:47; :: thesis: verum

end;A382: (dom f) /\ B c= (dom f) /\ A by A372, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: a <= g . x

then A383: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a <= f . x by A381, A382;

hence a <= g . x by A383, FUNCT_1:47; :: thesis: verum

consider a being Real such that

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

A386: (dom f) /\ B c= (dom f) /\ A by A372, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: g . x <= a

then A387: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a >= f . x by A385, A386;

hence g . x <= a by A387, FUNCT_1:47; :: thesis: verum

end;A386: (dom f) /\ B c= (dom f) /\ A by A372, XBOOLE_1:26;

assume x in B /\ (dom g) ; :: thesis: g . x <= a

then A387: x in dom g by XBOOLE_0:def 4;

then x in (dom f) /\ B by RELAT_1:61;

then a >= f . x by A385, A386;

hence g . x <= a by A387, FUNCT_1:47; :: thesis: verum

hence g | B is bounded by A384; :: thesis: verum

then A388: D1 . (j - 1) <= D . (i + 1) by A232, A245, A277, INTEGRA1:def 4;

A389: (j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A258, XREAL_1:233;

A390: len (upper_volume (g,MD1)) = len MD1 by INTEGRA1:def 6

.= (j - (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A356, A389, FINSEQ_6:118 ;

A391: j <= len H

A392: for k being Nat st 1 <= k & k <= len (upper_volume (g,MD1)) holds

(upper_volume (g,MD1)) . k = (mid (H

proof

n1 + 1 <= len H
let k be Nat; :: thesis: ( 1 <= k & k <= len (upper_volume (g,MD1)) implies (upper_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k )

assume that

A393: 1 <= k and

A394: k <= len (upper_volume (g,MD1)) ; :: thesis: (upper_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k

k in Seg (len (upper_volume (g,MD1))) by A393, A394, FINSEQ_1:1;

then A395: k in Seg (len MD1) by INTEGRA1:def 6;

then A396: k in dom MD1 by FINSEQ_1:def 3;

k in dom MD1 by A395, FINSEQ_1:def 3;

then A397: (upper_volume (g,MD1)) . k = (upper_bound (rng (g | (divset (MD1,k))))) * (vol (divset (MD1,k))) by INTEGRA1:def 6;

consider k2 being Element of NAT such that

A398: n1 + 1 = 1 + k2 ;

A399: 1 <= k + k2 by A393, NAT_1:12;

k <= j - ((n1 + 1) - 1) by A390, A394;

then k + ((n1 + 1) - 1) <= j by XREAL_1:19;

then k + k2 <= len D1 by A264, A398, XXREAL_0:2;

then A400: k + k2 in Seg (len D1) by A399, FINSEQ_1:1;

then A401: k + k2 in dom D1 by FINSEQ_1:def 3;

1 + 1 <= k + k2 by A259, A393, A398, XREAL_1:7;

then A402: 1 < k + k2 by NAT_1:13;

A403: k2 = (n1 + 1) - 1 by A398;

A404: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )

then A412: divset (D1,(k + k2)) = divset (MD1,k) by A404, INTEGRA1:4;

A413: k + k2 in dom D1 by A400, FINSEQ_1:def 3;

A414: (mid (H_{1}(D1),(n1 + 1),j)) . k =
H_{1}(D1) . ((k + (n1 + 1)) - 1)
by A258, A244, A390, A391, A393, A394, FINSEQ_6:122

.= (upper_bound (rng (f | (divset (D1,(k + k2)))))) * (vol (divset (D1,(k + k2)))) by A398, A413, INTEGRA1:def 6 ;

k in dom MD1 by A395, FINSEQ_1:def 3;

then divset (D1,(k + k2)) c= B by A412, INTEGRA1:8;

hence (upper_volume (g,MD1)) . k = (mid (H_{1}(D1),(n1 + 1),j)) . k
by A397, A414, A412, FUNCT_1:51; :: thesis: verum

end;assume that

A393: 1 <= k and

A394: k <= len (upper_volume (g,MD1)) ; :: thesis: (upper_volume (g,MD1)) . k = (mid (H

k in Seg (len (upper_volume (g,MD1))) by A393, A394, FINSEQ_1:1;

then A395: k in Seg (len MD1) by INTEGRA1:def 6;

then A396: k in dom MD1 by FINSEQ_1:def 3;

k in dom MD1 by A395, FINSEQ_1:def 3;

then A397: (upper_volume (g,MD1)) . k = (upper_bound (rng (g | (divset (MD1,k))))) * (vol (divset (MD1,k))) by INTEGRA1:def 6;

consider k2 being Element of NAT such that

A398: n1 + 1 = 1 + k2 ;

A399: 1 <= k + k2 by A393, NAT_1:12;

k <= j - ((n1 + 1) - 1) by A390, A394;

then k + ((n1 + 1) - 1) <= j by XREAL_1:19;

then k + k2 <= len D1 by A264, A398, XXREAL_0:2;

then A400: k + k2 in Seg (len D1) by A399, FINSEQ_1:1;

then A401: k + k2 in dom D1 by FINSEQ_1:def 3;

1 + 1 <= k + k2 by A259, A393, A398, XREAL_1:7;

then A402: 1 < k + k2 by NAT_1:13;

A403: k2 = (n1 + 1) - 1 by A398;

A404: ( 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 A405:
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 A396, INTEGRA1:def 4;

then A406: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A390, A393, A394, FINSEQ_6:122;

lower_bound (divset (MD1,k)) = D1 . n1 by A353, A396, A405, 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 A403, A402, A401, A405, A406, INTEGRA1:def 4; :: thesis: verum

end;then A406: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A390, A393, A394, FINSEQ_6:122;

lower_bound (divset (MD1,k)) = D1 . n1 by A353, A396, A405, 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 A403, A402, A401, A405, A406, INTEGRA1:def 4; :: thesis: verum

suppose A407:
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 A396, INTEGRA1:def 4;

then A408: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A390, A393, A394, FINSEQ_6:122;

A409: k - 1 <= (j - (n1 + 1)) + 1 by A390, A394, XREAL_1:146, XXREAL_0:2;

A410: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A396, A407, INTEGRA1:def 4;

A411: k - 1 in dom MD1 by A396, A407, INTEGRA1:7;

then 1 <= k - 1 by FINSEQ_3:25;

then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A258, A264, A244, A356, A411, A409, A410, 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 A398, A402, A401, A408, INTEGRA1:def 4; :: thesis: verum

end;then A408: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A390, A393, A394, FINSEQ_6:122;

A409: k - 1 <= (j - (n1 + 1)) + 1 by A390, A394, XREAL_1:146, XXREAL_0:2;

A410: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A396, A407, INTEGRA1:def 4;

A411: k - 1 in dom MD1 by A396, A407, INTEGRA1:7;

then 1 <= k - 1 by FINSEQ_3:25;

then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A258, A264, A244, A356, A411, A409, A410, 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 A398, A402, A401, A408, INTEGRA1:def 4; :: thesis: verum

then A412: divset (D1,(k + k2)) = divset (MD1,k) by A404, INTEGRA1:4;

A413: k + k2 in dom D1 by A400, FINSEQ_1:def 3;

A414: (mid (H

.= (upper_bound (rng (f | (divset (D1,(k + k2)))))) * (vol (divset (D1,(k + k2)))) by A398, A413, INTEGRA1:def 6 ;

k in dom MD1 by A395, FINSEQ_1:def 3;

then divset (D1,(k + k2)) c= B by A412, INTEGRA1:8;

hence (upper_volume (g,MD1)) . k = (mid (H

then len (upper_volume (g,MD1)) = len (mid (H

then A415: Sum (upper_volume (g,MD1)) = Sum (mid (H

A416: n1 < j - 1 by A348, XREAL_1:20;

A417: 1 <= (indx (D2,D1,n1)) + 1 by A263, NAT_1:13;

A418: len MD1 in dom MD1 by FINSEQ_5:6;

A419: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)

proof
end;

vol B = (upper_bound B) - (D1 . n1)
by A353, INTEGRA1:def 5;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 A418, 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 A418, INTEGRA1:def 4; :: thesis: verum

end;then vol B = (D1 . j) - (D1 . n1) by A232, A245, A277, A354, A363, A419, INTEGRA1:def 4;

then A420: vol B <> 0 by A232, A241, A245, SEQM_3:def 1;

rng f is bounded_below by A1, INTEGRA1:11;

then A421: 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 A421, XREAL_1:13;

then A422: ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) >= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A379, XREAL_1:64;

D1 . n1 < D1 . (n1 + 1) by A241, A266, A351, SEQM_3:def 1;

then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A262, A260, A270, A267, SEQ_4:137;

then A423: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,(n1 + 1)) by NAT_1:13;

then A424: (indx (D2,D1,n1)) + 1 <= len D2 by A274, XXREAL_0:2;

A425: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;

A426: indx (D2,D1,(n1 + 1)) = (indx (D2,D1,n1)) + 1

proof

A443:
len MD2 = ((indx (D2,D1,j)) -' (indx (D2,D1,(n1 + 1)))) + 1
by A275, A271, A274, A238, A239, A357, FINSEQ_6:118;
assume
indx (D2,D1,(n1 + 1)) <> (indx (D2,D1,n1)) + 1
; :: thesis: contradiction

then A427: indx (D2,D1,(n1 + 1)) > (indx (D2,D1,n1)) + 1 by A423, XXREAL_0:1;

A428: (indx (D2,D1,n1)) + 1 in dom D2 by A417, A424, FINSEQ_3:25;

then A429: D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by FUNCT_1:def 3;

end;then A427: indx (D2,D1,(n1 + 1)) > (indx (D2,D1,n1)) + 1 by A423, XXREAL_0:1;

A428: (indx (D2,D1,n1)) + 1 in dom D2 by A417, A424, FINSEQ_3:25;

then A429: 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 A11, A429, 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

A430: n2 in dom D1 and

A431: D2 . ((indx (D2,D1,n1)) + 1) = D1 . n2 by PARTFUN1:3;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A262, A425, A428, SEQM_3:def 1;

then n1 < n2 by A241, A260, A430, A431, SEQ_4:137;

then A432: n1 + 1 <= n2 by NAT_1:13;

D1 . n2 < D1 . (n1 + 1) by A270, A267, A427, A428, A431, SEQM_3:def 1;

hence contradiction by A266, A430, A432, SEQ_4:137; :: thesis: verum

end;A430: n2 in dom D1 and

A431: D2 . ((indx (D2,D1,n1)) + 1) = D1 . n2 by PARTFUN1:3;

D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A262, A425, A428, SEQM_3:def 1;

then n1 < n2 by A241, A260, A430, A431, SEQ_4:137;

then A432: n1 + 1 <= n2 by NAT_1:13;

D1 . n2 < D1 . (n1 + 1) by A270, A267, A427, A428, A431, SEQM_3:def 1;

hence contradiction by A266, A430, A432, SEQ_4:137; :: thesis: verum

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

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

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

A436: n2 in dom D and

A437: D2 . ((indx (D2,D1,n1)) + 1) = D . n2 by A433, PARTFUN1:3;

D1 . n1 < D . n2 by A262, A260, A425, A428, A437, SEQM_3:def 1;

then D . i < D . n2 by A434, A435, XXREAL_0:2;

then i < n2 by A236, A436, SEQ_4:137;

then A438: i + 1 <= n2 by NAT_1:13;

(n1 + 1) + 1 <= j by A348, NAT_1:13;

then A439: n1 + 1 <= j - 1 by XREAL_1:19;

j - 1 in dom D1 by A232, A245, A277, INTEGRA1:7;

then A440: D1 . (n1 + 1) <= D1 . (j - 1) by A266, A439, SEQ_4:137;

A441: lower_bound (divset (D1,j)) <= D . (i + 1) by A233, INTEGRA2:1;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 4;

then A442: D1 . (n1 + 1) <= D . (i + 1) by A440, A441, XXREAL_0:2;

D . n2 < D1 . (n1 + 1) by A270, A267, A427, A428, A437, SEQM_3:def 1;

then D . n2 < D . (i + 1) by A442, XXREAL_0:2;

hence contradiction by A231, A436, A438, SEQ_4:137; :: thesis: verum

end;A435: upper_bound (divset (D1,n1)) = D1 . n1

proof
end;

consider n2 being Element of NAT such that A436: n2 in dom D and

A437: D2 . ((indx (D2,D1,n1)) + 1) = D . n2 by A433, PARTFUN1:3;

D1 . n1 < D . n2 by A262, A260, A425, A428, A437, SEQM_3:def 1;

then D . i < D . n2 by A434, A435, XXREAL_0:2;

then i < n2 by A236, A436, SEQ_4:137;

then A438: i + 1 <= n2 by NAT_1:13;

(n1 + 1) + 1 <= j by A348, NAT_1:13;

then A439: n1 + 1 <= j - 1 by XREAL_1:19;

j - 1 in dom D1 by A232, A245, A277, INTEGRA1:7;

then A440: D1 . (n1 + 1) <= D1 . (j - 1) by A266, A439, SEQ_4:137;

A441: lower_bound (divset (D1,j)) <= D . (i + 1) by A233, INTEGRA2:1;

lower_bound (divset (D1,j)) = D1 . (j - 1) by A232, A245, A277, INTEGRA1:def 4;

then A442: D1 . (n1 + 1) <= D . (i + 1) by A440, A441, XXREAL_0:2;

D . n2 < D1 . (n1 + 1) by A270, A267, A427, A428, A437, SEQM_3:def 1;

then D . n2 < D . (i + 1) by A442, XXREAL_0:2;

hence contradiction by A231, A436, A438, SEQ_4:137; :: thesis: verum

then A444: len MD2 = ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by A275, XREAL_1:233;

then A445: len (upper_volume (g,MD2)) = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A426, INTEGRA1:def 6;

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;

A449: len MD1 = (j -' (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A356, FINSEQ_6:118;

then ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A258, XREAL_1:233

.= j ;

then A450: MD1 . (len MD1) = D1 . j by A258, A264, A244, A356, A448, A449, FINSEQ_6:122;

rng MD1 c= rng D1 by A356, FINSEQ_6:119;

then A451: x1 in rng D1 by A447;

rng D1 c= rng D2 by A10, INTEGRA1:def 18;

then consider k being Element of NAT such that

A452: k in dom D2 and

A453: D2 . k = x1 by A451, PARTFUN1:3;

x1 <= MD1 . (len MD1) by A447, Th16;

then k <= indx (D2,D1,j) by A237, A234, A450, A452, A453, 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 A454: (k - (indx (D2,D1,(n1 + 1)))) + 1 <= ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by XREAL_1:6;

A455: MD1 . 1 <= x1 by A447, Th16;

MD1 . 1 = D1 . (n1 + 1) by A261, A264, A244, A265, A356, FINSEQ_6:118;

then A456: indx (D2,D1,(n1 + 1)) <= k by A270, A267, A455, A452, A453, SEQM_3:def 1;

then consider n being Nat such that

A457: k + 1 = (indx (D2,D1,(n1 + 1))) + n by NAT_1:10, NAT_1:12;

A458: (n + (indx (D2,D1,(n1

then 1 in dom MD1 by FINSEQ_3:32;

then A448: 1 <= len MD1 by FINSEQ_3:25;

A449: len MD1 = (j -' (n1 + 1)) + 1 by A258, A261, A264, A244, A265, A356, FINSEQ_6:118;

then ((len MD1) + (n1 + 1)) - 1 = (((j - (n1 + 1)) + 1) + (n1 + 1)) - 1 by A258, XREAL_1:233

.= j ;

then A450: MD1 . (len MD1) = D1 . j by A258, A264, A244, A356, A448, A449, FINSEQ_6:122;

rng MD1 c= rng D1 by A356, FINSEQ_6:119;

then A451: x1 in rng D1 by A447;

rng D1 c= rng D2 by A10, INTEGRA1:def 18;

then consider k being Element of NAT such that

A452: k in dom D2 and

A453: D2 . k = x1 by A451, PARTFUN1:3;

x1 <= MD1 . (len MD1) by A447, Th16;

then k <= indx (D2,D1,j) by A237, A234, A450, A452, A453, 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 A454: (k - (indx (D2,D1,(n1 + 1)))) + 1 <= ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by XREAL_1:6;

A455: MD1 . 1 <= x1 by A447, Th16;

MD1 . 1 = D1 . (n1 + 1) by A261, A264, A244, A265, A356, FINSEQ_6:118;

then A456: indx (D2,D1,(n1 + 1)) <= k by A270, A267, A455, A452, A453, SEQM_3:def 1;

then consider n being Nat such that

A457: k + 1 = (indx (D2,D1,(n1 + 1))) + n by NAT_1:10, NAT_1:12;

A458: (n + (indx (D2,D1,(n1