let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is convergent_to_0 & vol A <> 0 holds
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
let f be Function of A,REAL; :: thesis: for T being DivSequence of A st f | A is bounded & delta T is convergent_to_0 & vol A <> 0 holds
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
let T be DivSequence of A; :: thesis: ( f | A is bounded & delta T is convergent_to_0 & vol A <> 0 implies ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
assume A1: f | A is bounded ; :: thesis: ( not delta T is convergent_to_0 or not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
A2: for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) )
proof
let D, D1 be Division of A; :: thesis: 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)) )
consider D2 being Division of A such that
A3: D <= D2 and
A4: D1 <= D2 and
A5: rng D2 = (rng D1) \/ (rng D) by Th4;
A6: (upper_sum (f,D1)) - (upper_sum (f,D2)) >= 0 by A1, A4, INTEGRA1:45, XREAL_1:48;
(upper_sum (f,D)) - (upper_sum (f,D2)) >= 0 by A1, A3, INTEGRA1:45, XREAL_1:48;
hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) ) by A3, A4, A5, A6; :: thesis: verum
end;
A7: for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds
ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )
proof
let D, D1 be Division of A; :: thesis: ( 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)
proof
deffunc H1( Division of A) -> FinSequence of REAL = upper_volume (f,$1);
deffunc H2( Division of A, Nat) -> Element of REAL = (PartSums (upper_volume (f,$1))) . $2;
A12: len D2 in dom D2 by FINSEQ_5:6;
A13: for i being Element of NAT st i in dom D holds
ex j being Element of NAT st
( j in dom D1 & D . i in divset (D1,j) & H2(D1,j) - H2(D2, indx (D2,D1,j)) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )
proof
defpred S1[ non empty Nat] means ( $1 in dom D implies ex j being Element of NAT st
( j in dom D1 & D . $1 in divset (D1,j) & H2(D1,j) - H2(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) & H2(D1,j) - H2(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) & H2(D1,j) - H2(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
proof
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)))
proof
per cases ( i = 1 or i <> 1 ) ;
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;
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;
end;
end;
hence contradiction by A8; :: thesis: verum
end;
A36: S1[1]
proof
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;
H2(D1,j) - H2(D2, indx (D2,D1,j)) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)
proof
A40: j <> 1 by A16, A37, A38, A39;
then reconsider j1 = j - 1 as Element of NAT by A38, INTEGRA1: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
A51: (indx (D2,D1,j)) - (indx (D2,D1,j1)) <= 2
proof
reconsider ID1 = (indx (D2,D1,j1)) + 1 as Element of NAT ;
reconsider ID2 = ID1 + 1 as Element of NAT ;
assume (indx (D2,D1,j)) - (indx (D2,D1,j1)) > 2 ; :: thesis: 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
assume A66: ( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 ) ; :: thesis: contradiction
per cases ( D2 . ID1 in rng D1 or D2 . ID2 in rng D1 ) by A66;
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;
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;
end;
end;
upper_bound (divset (D1,j)) = D1 . j by A38, A40, INTEGRA1:def 4;
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;
A78: 1 <= (indx (D2,D1,j1)) + 1 by A46, NAT_1:13;
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;
(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) = <*((upper_volume (f,D1)) . j)*> 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
per 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;
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;
(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))) = <*((upper_volume (f,D2)) . ((indx (D2,D1,j1)) + 1))*> 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;
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 = H1(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) -' 1) by A49, A84, A85, A78, A86, A100, FINSEQ_6:118
.= H1(D2) . ((2 + ((indx (D2,D1,j1)) + 1)) - 1) by A102, XREAL_1:233
.= H1(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 (H1(D1),j,j))) - (Sum (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * ((vol (divset (D2,((indx (D2,D1,j1)) + 2)))) + (vol (divset (D2,((indx (D2,D1,j1)) + 1)))))
proof
set ID2 = (indx (D2,D1,j1)) + 2;
set ID1 = (indx (D2,D1,j1)) + 1;
set SR = upper_bound (rng (f | (divset (D2,((indx (D2,D1,j1)) + 1)))));
set VR = vol (divset (D2,((indx (D2,D1,j1)) + 1)));
set B = vol (divset (D2,((indx (D2,D1,j1)) + 1)));
set C = vol (divset (D2,((indx (D2,D1,j1)) + 2)));
divset (D1,j) c= A by A38, INTEGRA1: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 number ;
A124: ((upper_volume (f,D1)) . j) - (A * (vol (divset (D2,((indx (D2,D1,j1)) + 1))))) = A * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A117;
(upper_bound (rng (f | (divset (D1,j))))) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) <= (upper_bound (rng f)) * (vol (divset (D2,((indx (D2,D1,j1)) + 2)))) by A106, A119, XREAL_1:64;
then Sum (mid (H1(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 (H1(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 (H1(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 (H1(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 (H1(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))))) + (H1(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 (H1(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 (H1(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 (H1(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 (H1(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 (H1(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 (H1(D1),j,j))) - (Sum (mid (H1(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 (H1(D1),j,j))) - (Sum (mid (H1(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;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
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;
end;
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: verum
end;
j < j + 1 by NAT_1:13;
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 set st x1 in rng (D1 | j1) holds
x1 in rng (D2 | (indx (D2,D1,j1)))
proof
let x1 be set ; :: 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;
then A145: rng (D1 | j1) c= rng (D2 | (indx (D2,D1,j1))) by TARSKI:def 3;
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 set st x1 in rng (D2 | (indx (D2,D1,j1))) holds
x1 in rng (D1 | j1)
proof
let x1 be set ; :: 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) )
proof
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;
A160: ( D2 . k in rng D implies D2 . k = D1 . j1 )
proof
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;
A163: ( D2 . k in rng D implies D2 . k in rng (D1 | j1) )
proof
j1 in Seg (len (D1 | j1)) by A146, A152, FINSEQ_1: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;
D2 . k in rng D2 by A151, FUNCT_1:def 3;
hence x1 in rng (D1 | j1) by A11, A44, A149, A150, A163, A154, RFINSEQ:6, XBOOLE_0:def 3; :: thesis: verum
end;
then rng (D2 | (indx (D2,D1,j1))) c= rng (D1 | j1) by TARSKI:def 3;
then A166: rng (D2 | (indx (D2,D1,j1))) = rng (D1 | j1) by A145, XBOOLE_0:def 10;
mid (D1,1,j1) is increasing by A38, A40, A146, INTEGRA1: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
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
now
per cases ( k > indx (D2,D1,k) or k < indx (D2,D1,k) ) by A172, XXREAL_0:1;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
A187: for k being Nat st 1 <= k & k <= len ((upper_volume (f,D1)) | j1) holds
((upper_volume (f,D1)) | j1) . k = ((upper_volume (f,D2)) | (indx (D2,D1,j1))) . k
proof
indx (D2,D1,j1) in Seg (len D2) by A44, FINSEQ_1:def 3;
then indx (D2,D1,j1) in Seg (len (upper_volume (f,D2))) by INTEGRA1:def 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
per cases ( k = 1 or k <> 1 ) ;
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;
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;
end;
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;
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;
indx (D2,D1,j1) in dom D2 by A10, A43, INTEGRA1:def 19;
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 H1(D2)) by A128, INTEGRA1:def 6;
then A221: indx (D2,D1,j) in dom H1(D2) by FINSEQ_1:def 3;
indx (D2,D1,j) <= len D2 by A128, FINSEQ_1:1;
then A222: indx (D2,D1,j) <= len H1(D2) by INTEGRA1:def 6;
j in Seg (len H1(D1)) by A219, INTEGRA1:def 6;
then A223: j in dom H1(D1) by FINSEQ_1:def 3;
j <= len D1 by A219, FINSEQ_1:1;
then A224: j <= len H1(D1) by INTEGRA1:def 6;
j1 in Seg (len D1) by A41, FINSEQ_1:def 3;
then j1 in Seg (len H1(D1)) by INTEGRA1:def 6;
then j1 in dom H1(D1) by FINSEQ_1:def 3;
then H2(D1,j1) = Sum (H1(D1) | j1) by INTEGRA1:def 20;
then H2(D1,j1) + (Sum (mid (H1(D1),j,j))) = Sum ((H1(D1) | j1) ^ (mid (H1(D1),j,j))) by RVSUM_1:75
.= Sum ((mid (H1(D1),1,j1)) ^ (mid (H1(D1),(j1 + 1),j))) by A146, FINSEQ_6:116
.= Sum (mid (H1(D1),1,j)) by A146, A224, A127, INTEGRA2:4
.= Sum (H1(D1) | j) by A220, FINSEQ_6:116 ;
then A225: H2(D1,j1) + (Sum (mid ((upper_volume (f,D1)),j,j))) = H2(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 H1(D2)) by INTEGRA1:def 6;
then indx (D2,D1,j1) in dom H1(D2) by FINSEQ_1:def 3;
then H2(D2, indx (D2,D1,j1)) = Sum (H1(D2) | (indx (D2,D1,j1))) by INTEGRA1:def 20;
then H2(D2, indx (D2,D1,j1)) + (Sum (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) = Sum ((H1(D2) | (indx (D2,D1,j1))) ^ (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) by RVSUM_1:75
.= Sum ((mid (H1(D2),1,(indx (D2,D1,j1)))) ^ (mid (H1(D2),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) by A46, FINSEQ_6:116
.= Sum (mid (H1(D2),1,(indx (D2,D1,j)))) by A46, A48, A222, INTEGRA2:4
.= Sum (H1(D2) | (indx (D2,D1,j))) by A129, FINSEQ_6:116 ;
then A226: H2(D2, indx (D2,D1,j1)) + (Sum (mid ((upper_volume (f,D2)),((indx (D2,D1,j1)) + 1),(indx (D2,D1,j))))) = H2(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 H2(D2, indx (D2,D1,j1)) = Sum ((upper_volume (f,D2)) | (indx (D2,D1,j1))) by INTEGRA1:def 20
.= H2(D1,j1) by A218, A42, INTEGRA1:def 20 ;
hence H2(D1,j) - H2(D2, indx (D2,D1,j)) <= (1 * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A50, A226, A225; :: thesis: verum
end;
hence S1[1] by A38, A39; :: thesis: verum
end;
reconsider i = i as non empty Element of NAT by A15, FINSEQ_1:1;
A227: for i being non empty Nat st S1[i] holds
S1[i + 1]
proof
let i be non empty Nat; :: thesis: ( S1[i] implies S1[i + 1] )
A228: i >= 1 by NAT_1:14;
assume A229: S1[i] ; :: thesis: S1[i + 1]
S1[i + 1]
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) & H2(D1,j) - H2(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 H1(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: H2(D1,n1) - H2(D2, indx (D2,D1,n1)) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A229, A235, FINSEQ_1:def 3;
A244: 1 <= n1 + 1 by NAT_1:12;
A245: n1 < j
proof
assume A246: n1 >= j ; :: thesis: contradiction
now
per cases ( n1 = j or n1 > j ) by A246, XXREAL_0:1;
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
proof
per cases ( j = 1 or j <> 1 ) ;
end;
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
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then A258: n1 + 1 <= j by NAT_1:13;
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 H1(D1) by A264, INTEGRA1:def 6;
then j in Seg (len H1(D1)) by A261, FINSEQ_1:1;
then A269: j in dom H1(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 H1(D1)) by INTEGRA1:def 6;
then n1 in dom H1(D1) by FINSEQ_1:def 3;
then H2(D1,n1) = Sum (H1(D1) | n1) by INTEGRA1:def 20
.= Sum (mid (H1(D1),1,n1)) by A259, FINSEQ_6:116 ;
then H2(D1,n1) + (Sum (mid (H1(D1),(n1 + 1),j))) = Sum ((mid (H1(D1),1,n1)) ^ (mid (H1(D1),(n1 + 1),j))) by RVSUM_1:75
.= Sum (mid (H1(D1),1,j)) by A245, A259, A268, INTEGRA2:4
.= Sum (H1(D1) | j) by A261, FINSEQ_6:116 ;
then A272: H2(D1,j) = H2(D1,n1) + (Sum (mid (H1(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 H1(D2)) by INTEGRA1:def 6;
then A273: indx (D2,D1,j) in dom H1(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 (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)
proof
per cases ( n1 + 1 = j or n1 + 1 < j ) by A258, XXREAL_0:1;
suppose A279: n1 + 1 = j ; :: thesis: (Sum (mid (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(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
proof
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
proof
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;
D2 . ((indx (D2,D1,n1)) + 2) in rng D2 by A288, FUNCT_1:def 3;
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
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;
D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by A299, FUNCT_1:def 3;
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;
A307: ( (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) implies (indx (D2,D1,n1)) + 2 = indx (D2,D1,j) )
proof
assume (indx (D2,D1,n1)) + 1 < indx (D2,D1,j) ; :: thesis: (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;
A309: 1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;
A310: indx (D2,D1,j) <= len H1(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 H1(D2) by INTEGRA1:def 6;
then A313: len (mid (H1(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 (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) >= (lower_bound (rng f)) * (vol (divset (D1,(n1 + 1))))
proof
now
per cases ( (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1 or (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2 ) by A314, A307;
suppose A316: (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 1 ; :: thesis: Sum (mid (H1(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;
1 = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A316;
then (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 1 = H1(D2) . ((1 + ((indx (D2,D1,n1)) + 1)) - 1) by A309, A310, FINSEQ_6:122
.= H1(D2) . ((indx (D2,D1,n1)) + 1) ;
then A322: mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*(H1(D2) . ((indx (D2,D1,n1)) + 1))*> by A313, A316, FINSEQ_1:40;
H1(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 H1(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 (H1(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;
suppose A323: (indx (D2,D1,j)) - (indx (D2,D1,n1)) = 2 ; :: thesis: Sum (mid (H1(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 H1(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 H1(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: H1(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 (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 2 = H1(D2) . ((2 + ((indx (D2,D1,n1)) + 1)) - 1) by A332, A333, A330, FINSEQ_6:122
.= H1(D2) . (((indx (D2,D1,n1)) + 0) + 2) ;
((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 >= 1 by A323;
then (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . 1 = H1(D2) . ((1 + ((indx (D2,D1,n1)) + 1)) - 1) by A323, A332, A333, A330, FINSEQ_6:122
.= H1(D2) . ((indx (D2,D1,n1)) + 1) ;
then mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))) = <*(H1(D2) . ((indx (D2,D1,n1)) + 1)),(H1(D2) . ((indx (D2,D1,n1)) + 2))*> by A313, A323, A336, FINSEQ_1:44;
then A337: Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) = (H1(D2) . ((indx (D2,D1,n1)) + 1)) + (H1(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;
H1(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 H1(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 (H1(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 (H1(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;
end;
end;
hence Sum (mid (H1(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 H1(D1) by A265, INTEGRA1:def 6;
(j -' (n1 + 1)) + 1 = (j - (n1 + 1)) + 1 by A279, XREAL_1:233;
then A342: len (mid (H1(D1),(n1 + 1),j)) = 1 by A244, A279, A341, FINSEQ_6:118;
(n1 + 1) + 1 <= j + 1 by A258, XREAL_1:6;
then 1 <= (j + 1) - (n1 + 1) by XREAL_1:19;
then (mid (H1(D1),(n1 + 1),j)) . 1 = H1(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 (H1(D1),(n1 + 1),j) = <*((upper_bound (rng (f | (divset (D1,(n1 + 1)))))) * (vol (divset (D1,(n1 + 1)))))*> by A342, FINSEQ_1:40;
then A343: Sum (mid (H1(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 (H1(D1),(n1 + 1),j)) <= (upper_bound (rng f)) * (vol (divset (D1,(n1 + 1)))) by A343, A344, XREAL_1:64;
then (Sum (mid (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(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 (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(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;
suppose A348: n1 + 1 < j ; :: thesis: (Sum (mid (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(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)) )
proof
per cases ( len MD1 = 1 or len MD1 <> 1 ) ;
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;
end;
end;
A372: B c= A
proof
let x1 be set ; :: 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;
then reconsider g = f | B as Function of B,REAL by FUNCT_2:32;
A379: delta MD1 >= 0 by Th9;
A380: g | B is bounded
proof
consider a being real number such that
A381: for x being set st x in A /\ (dom f) holds
a <= f . x by A1, RFUNCT_1:71;
for x being set st x in B /\ (dom g) holds
a <= g . x
proof
let x be set ; :: 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;
then A384: g | B is bounded_below by RFUNCT_1:71;
consider a being real number such that
A385: for x being set st x in A /\ (dom f) holds
f . x <= a by A1, RFUNCT_1:70;
for x being set st x in B /\ (dom g) holds
g . x <= a
proof
let x be set ; :: 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;
then g | B is bounded_above by RFUNCT_1:70;
hence g | B is bounded by A384; :: thesis: verum
end;
lower_bound (divset (D1,j)) <= D . (i + 1) by A233, INTEGRA2:1;
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 H1(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 (H1(D1),(n1 + 1),j)) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len (upper_volume (g,MD1)) implies (upper_volume (g,MD1)) . k = (mid (H1(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 (H1(D1),(n1 + 1),j)) . k
A395: k in Seg (len (upper_volume (g,MD1))) by A393, A394, FINSEQ_1:1;
then A396: k in Seg (len MD1) by INTEGRA1:def 6;
then A397: k in dom MD1 by FINSEQ_1:def 3;
k in dom MD1 by A396, FINSEQ_1:def 3;
then A398: (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
A399: n1 + 1 = 1 + k2 ;
A400: 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, A399, XXREAL_0:2;
then A401: k + k2 in Seg (len D1) by A400, FINSEQ_1:1;
then A402: k + k2 in dom D1 by FINSEQ_1:def 3;
1 + 1 <= k + k2 by A259, A393, A399, XREAL_1:7;
then A403: 1 < k + k2 by NAT_1:13;
A404: k2 = (n1 + 1) - 1 by A399;
A405: ( lower_bound (divset (D1,(k + k2))) = lower_bound (divset (MD1,k)) & upper_bound (divset (D1,(k + k2))) = upper_bound (divset (MD1,k)) )
proof
per cases ( k = 1 or k <> 1 ) ;
suppose A406: 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 A397, INTEGRA1:def 4;
then A407: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A390, A393, A394, A395, FINSEQ_6:122;
lower_bound (divset (MD1,k)) = D1 . n1 by A353, A397, A406, 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 A404, A403, A402, A406, A407, INTEGRA1:def 4; :: thesis: verum
end;
suppose A408: 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 A397, INTEGRA1:def 4;
then A409: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A390, A393, A394, A395, FINSEQ_6:122;
A410: k - 1 <= (j - (n1 + 1)) + 1 by A390, A394, XREAL_1:146, XXREAL_0:2;
A411: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A397, A408, INTEGRA1:def 4;
A412: k - 1 in dom MD1 by A397, A408, 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, A412, A410, A411, 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 A399, A403, A402, A409, INTEGRA1:def 4; :: thesis: verum
end;
end;
end;
divset (MD1,k) = [.(lower_bound (divset (MD1,k))),(upper_bound (divset (MD1,k))).] by INTEGRA1:4;
then A413: divset (D1,(k + k2)) = divset (MD1,k) by A405, INTEGRA1:4;
A414: k + k2 in dom D1 by A401, FINSEQ_1:def 3;
A415: (mid (H1(D1),(n1 + 1),j)) . k = H1(D1) . ((k + (n1 + 1)) - 1) by A258, A244, A390, A391, A393, A394, A395, FINSEQ_6:122
.= (upper_bound (rng (f | (divset (D1,(k + k2)))))) * (vol (divset (D1,(k + k2)))) by A399, A414, INTEGRA1:def 6 ;
k in dom MD1 by A396, FINSEQ_1:def 3;
then divset (D1,(k + k2)) c= B by A413, INTEGRA1:8;
hence (upper_volume (g,MD1)) . k = (mid (H1(D1),(n1 + 1),j)) . k by A398, A415, A413, FUNCT_1:51; :: thesis: verum
end;
n1 + 1 <= len H1(D1) by A265, INTEGRA1:def 6;
then len (upper_volume (g,MD1)) = len (mid (H1(D1),(n1 + 1),j)) by A258, A261, A244, A389, A390, A391, FINSEQ_6:118;
then A416: Sum (upper_volume (g,MD1)) = Sum (mid (H1(D1),(n1 + 1),j)) by A392, FINSEQ_1:14;
A417: n1 < j - 1 by A348, XREAL_1:20;
A418: 1 <= (indx (D2,D1,n1)) + 1 by A263, NAT_1:13;
A419: len MD1 in dom MD1 by FINSEQ_5:6;
A420: upper_bound (divset (MD1,(len MD1))) = MD1 . (len MD1)
proof
per cases ( len MD1 = 1 or len MD1 <> 1 ) ;
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 A419, 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 A419, INTEGRA1:def 4; :: thesis: verum
end;
end;
end;
vol B = (upper_bound B) - (D1 . n1) by A353, INTEGRA1:def 5;
then vol B = (D1 . j) - (D1 . n1) by A232, A245, A277, A354, A363, A420, INTEGRA1:def 4;
then A421: vol B <> 0 by A232, A241, A245, SEQM_3:def 1;
rng f is bounded_below by A1, INTEGRA1:11;
then A422: 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 A422, XREAL_1:13;
then A423: ((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 A424: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,(n1 + 1)) by NAT_1:13;
then A425: (indx (D2,D1,n1)) + 1 <= len D2 by A274, XXREAL_0:2;
A426: indx (D2,D1,n1) < (indx (D2,D1,n1)) + 1 by NAT_1:13;
A427: indx (D2,D1,(n1 + 1)) = (indx (D2,D1,n1)) + 1
proof
assume indx (D2,D1,(n1 + 1)) <> (indx (D2,D1,n1)) + 1 ; :: thesis: contradiction
then A428: indx (D2,D1,(n1 + 1)) > (indx (D2,D1,n1)) + 1 by A424, XXREAL_0:1;
A429: (indx (D2,D1,n1)) + 1 in dom D2 by A418, A425, FINSEQ_3:25;
then A430: D2 . ((indx (D2,D1,n1)) + 1) in rng D2 by FUNCT_1:def 3;
now
per cases ( D2 . ((indx (D2,D1,n1)) + 1) in rng D1 or D2 . ((indx (D2,D1,n1)) + 1) in rng D ) by A11, A430, XBOOLE_0:def 3;
suppose D2 . ((indx (D2,D1,n1)) + 1) in rng D1 ; :: thesis: contradiction
then consider n2 being Element of NAT such that
A431: n2 in dom D1 and
A432: D2 . ((indx (D2,D1,n1)) + 1) = D1 . n2 by PARTFUN1:3;
D2 . (indx (D2,D1,n1)) < D2 . ((indx (D2,D1,n1)) + 1) by A262, A426, A429, SEQM_3:def 1;
then n1 < n2 by A241, A260, A431, A432, SEQ_4:137;
then A433: n1 + 1 <= n2 by NAT_1:13;
D1 . n2 < D1 . (n1 + 1) by A270, A267, A428, A429, A432, SEQM_3:def 1;
hence contradiction by A266, A431, A433, SEQ_4:137; :: thesis: verum
end;
suppose A434: D2 . ((indx (D2,D1,n1)) + 1) in rng D ; :: thesis: contradiction
A435: D . i <= upper_bound (divset (D1,n1)) by A242, INTEGRA2:1;
A436: upper_bound (divset (D1,n1)) = D1 . n1
proof
per cases ( n1 = 1 or n1 <> 1 ) ;
suppose n1 = 1 ; :: thesis: upper_bound (divset (D1,n1)) = D1 . n1
hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis: verum
end;
suppose n1 <> 1 ; :: thesis: upper_bound (divset (D1,n1)) = D1 . n1
hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis: verum
end;
end;
end;
consider n2 being Element of NAT such that
A437: n2 in dom D and
A438: D2 . ((indx (D2,D1,n1)) + 1) = D . n2 by A434, PARTFUN1:3;
D1 . n1 < D . n2 by A262, A260, A426, A429, A438, SEQM_3:def 1;
then D . i < D . n2 by A435, A436, XXREAL_0:2;
then i < n2 by A236, A437, SEQ_4:137;
then A439: i + 1 <= n2 by NAT_1:13;
(n1 + 1) + 1 <= j by A348, NAT_1:13;
then A440: n1 + 1 <= j - 1 by XREAL_1:19;
j - 1 in dom D1 by A232, A245, A277, INTEGRA1:7;
then A441: D1 . (n1 + 1) <= D1 . (j - 1) by A266, A440, SEQ_4:137;
A442: 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 A443: D1 . (n1 + 1) <= D . (i + 1) by A441, A442, XXREAL_0:2;
D . n2 < D1 . (n1 + 1) by A270, A267, A428, A429, A438, SEQM_3:def 1;
then D . n2 < D . (i + 1) by A443, XXREAL_0:2;
hence contradiction by A231, A437, A439, SEQ_4:137; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A444: len MD2 = ((indx (D2,D1,j)) -' (indx (D2,D1,(n1 + 1)))) + 1 by A275, A271, A274, A238, A239, A357, FINSEQ_6:118;
then A445: len MD2 = ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by A275, XREAL_1:233;
then A446: len (upper_volume (g,MD2)) = ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A427, INTEGRA1:def 6;
for x1 being set st x1 in (rng MD1) \/ {(D . (i + 1))} holds
x1 in rng MD2
proof
let x1 be set ; :: thesis: ( x1 in (rng MD1) \/ {(D . (i + 1))} implies x1 in rng MD2 )
assume A447: x1 in (rng MD1) \/ {(D . (i + 1))} ; :: thesis: x1 in rng MD2
then reconsider x1 = x1 as Real ;
now
per cases ( x1 in rng MD1 or x1 in {(D . (i + 1))} ) by A447, XBOOLE_0:def 3;
suppose A448: x1 in rng MD1 ; :: thesis: x1 in rng MD2
rng MD1 <> {} ;
then 1 in dom MD1 by FINSEQ_3:32;
then A449: 1 <= len MD1 by FINSEQ_3:25;
A450: 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 A451: MD1 . (len MD1) = D1 . j by A258, A264, A244, A356, A449, A450, FINSEQ_6:122;
rng MD1 c= rng D1 by A356, FINSEQ_6:119;
then A452: x1 in rng D1 by A448;
rng D1 c= rng D2 by A10, INTEGRA1:def 18;
then consider k being Element of NAT such that
A453: k in dom D2 and
A454: D2 . k = x1 by A452, PARTFUN1:3;
x1 <= MD1 . (len MD1) by A448, Th16;
then k <= indx (D2,D1,j) by A237, A234, A451, A453, A454, SEQM_3:def 1;
then k - (indx (D2,D1,(n1 + 1))) <= (indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1))) by XREAL_1:9;
then A455: (k - (indx (D2,D1,(n1 + 1)))) + 1 <= ((indx (D2,D1,j)) - (indx (D2,D1,(n1 + 1)))) + 1 by XREAL_1:6;
A456: MD1 . 1 <= x1 by A448, Th16;
MD1 . 1 = D1 . (n1 + 1) by A261, A264, A244, A265, A356, FINSEQ_6:118;
then A457: indx (D2,D1,(n1 + 1)) <= k by A270, A267, A456, A453, A454, SEQM_3:def 1;
then consider n being Nat such that
A458: k + 1 = (indx (D2,D1,(n1 + 1))) + n by NAT_1:10, NAT_1:12;
A459: (n + (indx (D2,D1,(n1 + 1)))) - 1 = k by A458;
A460: n in NAT by ORDINAL1:def 12;
(indx (D2,D1,(n1 + 1))) + 1 <= k + 1 by A457, XREAL_1:6;
then A461: 1 <= (k + 1) - (indx (D2,D1,(n1 + 1))) by XREAL_1:19;
then n in dom MD2 by A445, A455, A458, FINSEQ_3:25;
then MD2 . n in rng MD2 by FUNCT_1:def 3;
hence x1 in rng MD2 by A275, A271, A239, A357, A454, A461, A455, A460, A459, FINSEQ_6:122; :: thesis: verum
end;
suppose x1 in {(D . (i + 1))} ; :: thesis: x1 in rng MD2
then A462: x1 = D . (i + 1) by TARSKI:def 1;
reconsider j1 = j - 1 as Element of NAT by A232, A245, A277, INTEGRA1:7;
A463: rng D c= rng D2 by A9, INTEGRA1:def 18;
D . (i + 1) in rng D by A231, FUNCT_1:def 3;
then consider k being Element of NAT such that
A464: k in dom D2 and
A465: x1 = D2 . k by A462, A463, PARTFUN1:3;
D . (i + 1) <= upper_bound (divset (D1,j)) by A233, INTEGRA2:1;
then x1 <= D1 . j by A232, A245, A277, A462, INTEGRA1:def 4;
then A466: D2 . k <= D2 . (indx (D2,D1,j)) by A10, A232, A465, INTEGRA1:def 19;
n1 < j1 by A348, XREAL_1:20;
then A467: n1 + 1 <= j1 by NAT_1:13;
j - 1 in dom D1 by A232, A245, A277, INTEGRA1:7;
then A468: D1 . (n1 + 1) <= D1 . (j - 1) by A266, A467, SEQ_4:137;
lower_bound (divset (D1,j)) <= D . (i + 1) by A233, INTEGRA2:1;
then D1 . (j - 1) <= x1 by A232, A245, A277, A462, INTEGRA1:def 4;
then D2 . (indx (D2,D1,(n1 + 1))) <= D2 . k by A267, A465, A468, XXREAL_0:2;
hence x1 in rng MD2 by A270, A237, A357, A464, A465, A466, Th17; :: thesis: verum
end;
end;
end;
hence x1 in rng MD2 ; :: thesis: verum
end;
then A469: (rng MD1) \/ {(D . (i + 1))} c= rng MD2 by TARSKI:def 3;
rng MD2 <> {} ;
then 1 in dom MD2 by FINSEQ_3:32;
then A470: 1 <= len MD2 by FINSEQ_3:25;
A471: ((len MD2) - 1) + (indx (D2,D1,(n1 + 1))) = indx (D2,D1,j) by A445;
for x1 being set st x1 in rng MD2 holds
x1 in (rng MD1) \/ {(D . (i + 1))}
proof
let x1 be set ; :: thesis: ( x1 in rng MD2 implies x1 in (rng MD1) \/ {(D . (i + 1))} )
assume A472: x1 in rng MD2 ; :: thesis: x1 in (rng MD1) \/ {(D . (i + 1))}
then reconsider x1 = x1 as Real ;
A473: MD2 . 1 <= x1 by A472, Th16;
A474: MD2 . (len MD2) = D2 . (indx (D2,D1,j)) by A275, A271, A239, A357, A470, A444, A471, FINSEQ_6:122;
A475: rng MD2 c= rng D2 by A357, FINSEQ_6:119;
A476: MD2 . 1 = D2 . (indx (D2,D1,(n1 + 1))) by A271, A274, A238, A239, A357, FINSEQ_6:118;
A477: x1 <= MD2 . (len MD2) by A472, Th16;
then A478: x1 <= D1 . j by A234, A275, A271, A239, A357, A470, A444, A471, FINSEQ_6:122;
now
per cases ( x1 in rng D1 or x1 in rng D ) by A11, A472, A475, XBOOLE_0:def 3;
suppose x1 in rng D1 ; :: thesis: x1 in (rng MD1) \/ {(D . (i + 1))}
then consider k being Element of NAT such that
A479: k in dom D1 and
A480: D1 . k = x1 by PARTFUN1:3;
A481: n1 + 1 <= k by A266, A267, A473, A476, A479, A480, SEQM_3:def 1;
then A482: 1 <= k - n1 by XREAL_1:19;
n1 <= n1 + 1 by NAT_1:11;
then consider n being Nat such that
A483: k = n1 + n by A481, NAT_1:10, XXREAL_0:2;
A484: k <= j by A232, A234, A477, A474, A479, A480, SEQM_3:def 1;
then A485: k - n1 <= j - n1 by XREAL_1:9;
A486: 1 <= k - n1 by A481, XREAL_1:19;
A487: (j - (n1 + 1)) + 1 = j - n1 ;
k - n1 <= len MD1 by A358, A350, A484, XREAL_1:9;
then n in dom MD1 by A486, A483, FINSEQ_3:25;
then A488: MD1 . n in rng MD1 by FUNCT_1:def 3;
n in NAT by ORDINAL1:def 12;
then MD1 . n = D1 . (((k - n1) - 1) + (n1 + 1)) by A258, A264, A244, A356, A482, A485, A487, A483, FINSEQ_6:122
.= D1 . k ;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by A480, A488, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x1 in rng D ; :: thesis: x1 in (rng MD1) \/ {(D . (i + 1))}
then consider n being Element of NAT such that
A489: n in dom D and
A490: D . n = x1 by PARTFUN1:3;
A491: not i + 1 < n
proof
A492: upper_bound (divset (D1,j)) = D1 . j
proof
per cases ( j = 1 or j <> 1 ) ;
end;
end;
consider y1 being Real such that
A493: y1 = D . (i + 1) ;
A494: D . n in rng D by A489, FUNCT_1:def 3;
assume i + 1 < n ; :: thesis: contradiction
then A495: D . (i + 1) < D . n by A231, A489, SEQM_3:def 1;
lower_bound (divset (D1,j)) <= D . (i + 1) by A233, INTEGRA2:1;
then lower_bound (divset (D1,j)) <= D . n by A495, XXREAL_0:2;
then D . n in divset (D1,j) by A478, A490, A492, INTEGRA2:1;
then A496: x1 in (rng D) /\ (divset (D1,j)) by A490, A494, XBOOLE_0:def 4;
D . (i + 1) in rng D by A231, FUNCT_1:def 3;
then y1 in (rng D) /\ (divset (D1,j)) by A233, A493, XBOOLE_0:def 4;
hence contradiction by A8, A232, A490, A495, A496, A493, Th5; :: thesis: verum
end;
A497: upper_bound (divset (D1,n1)) = D1 . n1
proof
per cases ( n1 = 1 or n1 <> 1 ) ;
suppose n1 = 1 ; :: thesis: upper_bound (divset (D1,n1)) = D1 . n1
hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis: verum
end;
suppose n1 <> 1 ; :: thesis: upper_bound (divset (D1,n1)) = D1 . n1
hence upper_bound (divset (D1,n1)) = D1 . n1 by A241, INTEGRA1:def 4; :: thesis: verum
end;
end;
end;
D . i <= upper_bound (divset (D1,n1)) by A242, INTEGRA2:1;
then D . i < D1 . (n1 + 1) by A352, A497, XXREAL_0:2;
then D . i < D . n by A267, A473, A476, A490, XXREAL_0:2;
then i < n by A236, A489, SEQ_4:137;
then i + 1 <= n by NAT_1:13;
then ( i + 1 = n or i + 1 < n ) by XXREAL_0:1;
then x1 in {(D . (i + 1))} by A490, A491, TARSKI:def 1;
hence x1 in (rng MD1) \/ {(D . (i + 1))} by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence x1 in (rng MD1) \/ {(D . (i + 1))} ; :: thesis: verum
end;
then rng MD2 c= (rng MD1) \/ {(D . (i + 1))} by TARSKI:def 3;
then A498: rng MD2 = (rng MD1) \/ {(D . (i + 1))} by A469, XBOOLE_0:def 10;
delta MD1 in rng (upper_volume ((chi (B,B)),MD1)) by XXREAL_2:def 8;
then consider k being Element of NAT such that
A499: k in dom (upper_volume ((chi (B,B)),MD1)) and
A500: (upper_volume ((chi (B,B)),MD1)) . k = delta MD1 by PARTFUN1:3;
A501: k in Seg (len (upper_volume ((chi (B,B)),MD1))) by A499, FINSEQ_1:def 3;
then A502: k in Seg (len MD1) by INTEGRA1:def 6;
then A503: k in dom MD1 by FINSEQ_1:def 3;
A504: k <= len MD1 by A502, FINSEQ_1:1;
then k + n1 <= j by A358, A350, XREAL_1:19;
then A505: k + n1 <= len D1 by A264, XXREAL_0:2;
A506: 1 <= k by A501, FINSEQ_1:1;
A507: n1 + 1 > 1 by A277, NAT_1:13;
then n1 > 1 - 1 by XREAL_1:19;
then A508: k < k + n1 by XREAL_1:29;
then 1 < k + n1 by A506, XXREAL_0:2;
then A509: k + n1 in dom D1 by A505, FINSEQ_3:25;
( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) )
proof
per cases ( k = 1 or k <> 1 ) ;
suppose A510: k = 1 ; :: thesis: ( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) )
then upper_bound (divset (MD1,k)) = MD1 . k by A503, INTEGRA1:def 4;
then A511: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A358, A506, A504, FINSEQ_6:122;
lower_bound (divset (D1,(k + n1))) = D1 . ((k + n1) - 1) by A506, A508, A509, INTEGRA1:def 4;
hence ( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) ) by A353, A507, A503, A509, A510, A511, INTEGRA1:def 4; :: thesis: verum
end;
suppose A512: k <> 1 ; :: thesis: ( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) )
then upper_bound (divset (MD1,k)) = MD1 . k by A503, INTEGRA1:def 4;
then A513: upper_bound (divset (MD1,k)) = D1 . ((k + (n1 + 1)) - 1) by A258, A264, A244, A356, A358, A506, A504, FINSEQ_6:122;
A514: lower_bound (divset (MD1,k)) = MD1 . (k - 1) by A503, A512, INTEGRA1:def 4;
A515: k - 1 in dom MD1 by A503, A512, INTEGRA1:7;
then A516: k - 1 <= len MD1 by FINSEQ_3:25;
1 <= k - 1 by A515, FINSEQ_3:25;
then lower_bound (divset (MD1,k)) = D1 . (((k - 1) + (n1 + 1)) - 1) by A258, A264, A244, A356, A358, A515, A516, A514, FINSEQ_6:122;
hence ( lower_bound (divset (MD1,k)) = lower_bound (divset (D1,(k + n1))) & upper_bound (divset (MD1,k)) = upper_bound (divset (D1,(k + n1))) ) by A506, A508, A509, A513, INTEGRA1:def 4; :: thesis: verum
end;
end;
end;
then divset (MD1,k) = [.(lower_bound (divset (D1,(k + n1)))),(upper_bound (divset (D1,(k + n1)))).] by INTEGRA1:4;
then A517: divset (MD1,k) = divset (D1,(k + n1)) by INTEGRA1:4;
k + n1 in Seg (len D1) by A509, FINSEQ_1:def 3;
then k + n1 in Seg (len (upper_volume ((chi (A,A)),D1))) by INTEGRA1:def 6;
then A518: k + n1 in dom (upper_volume ((chi (A,A)),D1)) by FINSEQ_1:def 3;
k in dom MD1 by A502, FINSEQ_1:def 3;
then delta MD1 = vol (divset (MD1,k)) by A500, INTEGRA1:20;
then delta MD1 = (upper_volume ((chi (A,A)),D1)) . (k + n1) by A509, A517, INTEGRA1:20;
then delta MD1 in rng (upper_volume ((chi (A,A)),D1)) by A518, FUNCT_1:def 3;
then delta MD1 <= max (rng (upper_volume ((chi (A,A)),D1))) by XXREAL_2:def 8;
then A519: delta MD1 <= delta D1 ;
A520: D . (i + 1) <= upper_bound (divset (D1,j)) by A233, INTEGRA2:1;
lower_bound (divset (D1,j)) <= D . (i + 1) by A233, INTEGRA2:1;
then A521: D . (i + 1) in divset (MD1,(len MD1)) by A363, A520, INTEGRA2:1;
j - 1 in dom D1 by A232, A245, A277, INTEGRA1:7;
then D1 . n1 < D1 . (j - 1) by A241, A417, SEQM_3:def 1;
then D . (i + 1) > lower_bound B by A353, A388, XXREAL_0:2;
then (Sum (upper_volume (g,MD1))) - (Sum (upper_volume (g,MD2))) <= ((upper_bound (rng g)) - (lower_bound (rng g))) * (delta MD1) by A355, A380, A498, A521, A421, Th14;
then A522: (Sum (upper_volume (g,MD1))) - (Sum (upper_volume (g,MD2))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) by A423, XXREAL_0:2;
A523: indx (D2,D1,j) <= len H1(D2) by A239, INTEGRA1:def 6;
A524: (indx (D2,D1,n1)) + 1 <= indx (D2,D1,j) by A275, A424, XXREAL_0:2;
A525: for k being Nat st 1 <= k & k <= len (upper_volume (g,MD2)) holds
(upper_volume (g,MD2)) . k = (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len (upper_volume (g,MD2)) implies (upper_volume (g,MD2)) . k = (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k )
assume that
A526: 1 <= k and
A527: k <= len (upper_volume (g,MD2)) ; :: thesis: (upper_volume (g,MD2)) . k = (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k
A528: k in Seg (len (upper_volume (g,MD2))) by A526, A527, FINSEQ_1:1;
then A529: (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k = H1(D2) . ((k + ((indx (D2,D1,n1)) + 1)) - 1) by A418, A446, A523, A524, A526, A527, FINSEQ_6:122;
A530: k in Seg (len MD2) by A528, INTEGRA1:def 6;
then k in dom MD2 by FINSEQ_1:def 3;
then A531: (upper_volume (g,MD2)) . k = (upper_bound (rng (g | (divset (MD2,k))))) * (vol (divset (MD2,k))) by INTEGRA1:def 6;
1 <= (indx (D2,D1,n1)) + 1 by NAT_1:12;
then 1 + 1 <= k + ((indx (D2,D1,n1)) + 1) by A526, XREAL_1:7;
then A532: 1 <= (k + ((indx (D2,D1,n1)) + 1)) - 1 by XREAL_1:19;
consider k2 being Element of NAT such that
A533: (indx (D2,D1,n1)) + 1 = 1 + k2 ;
k <= (indx (D2,D1,j)) - (((indx (D2,D1,n1)) + 1) - 1) by A445, A427, A527, INTEGRA1:def 6;
then k + (((indx (D2,D1,n1)) + 1) - 1) <= indx (D2,D1,j) by XREAL_1:19;
then (k + ((indx (D2,D1,n1)) + 1)) - 1 <= len H1(D2) by A523, XXREAL_0:2;
then k + k2 in Seg (len H1(D2)) by A532, A533, FINSEQ_1:1;
then A534: k + k2 in Seg (len D2) by INTEGRA1:def 6;
then k + k2 in dom D2 by FINSEQ_1:def 3;
then A535: (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k = (upper_bound (rng (f | (divset (D2,(k + k2)))))) * (vol (divset (D2,(k + k2)))) by A529, A533, INTEGRA1:def 6;
A536: ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) )
proof
k + k2 >= 1 + 1 by A263, A526, A533, XREAL_1:7;
then A537: k + k2 > 1 by NAT_1:13;
A538: k in dom MD2 by A530, FINSEQ_1:def 3;
A539: k + k2 in dom D2 by A534, FINSEQ_1:def 3;
per cases ( k = 1 or k <> 1 ) ;
suppose A540: k = 1 ; :: thesis: ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) )
then A541: upper_bound (divset (D2,(k + k2))) = D2 . (1 + k2) by A537, A539, INTEGRA1:def 4;
A542: lower_bound (divset (MD2,k)) = lower_bound B by A538, A540, INTEGRA1:def 4;
upper_bound (divset (MD2,k)) = MD2 . k by A538, A540, INTEGRA1:def 4;
then A543: upper_bound (divset (MD2,k)) = D2 . ((1 + (indx (D2,D1,(n1 + 1)))) - 1) by A275, A239, A357, A418, A427, A446, A527, A540, FINSEQ_6:122
.= D1 . (n1 + 1) by A10, A266, INTEGRA1:def 19 ;
lower_bound (divset (D2,(k + k2))) = D2 . ((1 + k2) - 1) by A537, A539, A540, INTEGRA1:def 4;
hence ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) ) by A10, A241, A266, A353, A427, A533, A542, A543, A541, INTEGRA1:def 19; :: thesis: verum
end;
suppose A544: k <> 1 ; :: thesis: ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) )
then upper_bound (divset (MD2,k)) = MD2 . k by A538, INTEGRA1:def 4;
then A545: upper_bound (divset (MD2,k)) = D2 . ((k + ((indx (D2,D1,n1)) + 1)) - 1) by A275, A239, A357, A418, A427, A446, A526, A527, A528, FINSEQ_6:122;
A546: k - 1 <= ((indx (D2,D1,j)) - ((indx (D2,D1,n1)) + 1)) + 1 by A446, A527, XREAL_1:146, XXREAL_0:2;
A547: lower_bound (divset (MD2,k)) = MD2 . (k - 1) by A538, A544, INTEGRA1:def 4;
A548: k - 1 in dom MD2 by A538, A544, INTEGRA1:7;
then 1 <= k - 1 by FINSEQ_3:25;
then lower_bound (divset (MD2,k)) = D2 . (((k - 1) + ((indx (D2,D1,n1)) + 1)) - 1) by A275, A239, A357, A418, A427, A548, A546, A547, FINSEQ_6:122;
hence ( lower_bound (divset (MD2,k)) = lower_bound (divset (D2,(k + k2))) & upper_bound (divset (MD2,k)) = upper_bound (divset (D2,(k + k2))) ) by A533, A537, A539, A545, INTEGRA1:def 4; :: thesis: verum
end;
end;
end;
divset (MD2,k) = [.(lower_bound (divset (MD2,k))),(upper_bound (divset (MD2,k))).] by INTEGRA1:4;
then A549: divset (MD2,k) = divset (D2,(k + k2)) by A536, INTEGRA1:4;
k in dom MD2 by A530, FINSEQ_1:def 3;
then divset (D2,(k + k2)) c= B by A549, INTEGRA1:8;
hence (upper_volume (g,MD2)) . k = (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) . k by A531, A535, A549, FUNCT_1:51; :: thesis: verum
end;
(indx (D2,D1,n1)) + 1 <= len H1(D2) by A425, INTEGRA1:def 6;
then len (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) = ((indx (D2,D1,j)) -' ((indx (D2,D1,n1)) + 1)) + 1 by A238, A418, A523, A524, FINSEQ_6:118;
then len (upper_volume (g,MD2)) = len (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) by A275, A424, A446, XREAL_1:233, XXREAL_0:2;
then A550: Sum (upper_volume (g,MD2)) = Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))) by A525, FINSEQ_1:14;
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
then ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta MD1) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A519, XREAL_1:64;
hence (Sum (mid (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) <= ((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1) by A522, A550, A416, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then A551: (H2(D1,n1) - H2(D2, indx (D2,D1,n1))) + ((Sum (mid (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))))) <= ((i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)) + (((upper_bound (rng f)) - (lower_bound (rng f))) * (delta D1)) by A243, XREAL_1:7;
n1 < n1 + 1 by NAT_1:13;
then D1 . n1 < D1 . (n1 + 1) by A241, A266, SEQM_3:def 1;
then indx (D2,D1,n1) < indx (D2,D1,(n1 + 1)) by A262, A260, A270, A267, SEQ_4:137;
then A552: indx (D2,D1,n1) < indx (D2,D1,j) by A275, XXREAL_0:2;
indx (D2,D1,n1) in Seg (len D2) by A262, FINSEQ_1:def 3;
then indx (D2,D1,n1) in Seg (len H1(D2)) by INTEGRA1:def 6;
then indx (D2,D1,n1) in dom H1(D2) by FINSEQ_1:def 3;
then H2(D2, indx (D2,D1,n1)) = Sum (H1(D2) | (indx (D2,D1,n1))) by INTEGRA1:def 20
.= Sum (mid (H1(D2),1,(indx (D2,D1,n1)))) by A263, FINSEQ_6:116 ;
then H2(D2, indx (D2,D1,n1)) + (Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) = Sum ((mid (H1(D2),1,(indx (D2,D1,n1)))) ^ (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) by RVSUM_1:75
.= Sum (mid (H1(D2),1,(indx (D2,D1,j)))) by A263, A552, A240, INTEGRA2:4
.= Sum (H1(D2) | (indx (D2,D1,j))) by A238, FINSEQ_6:116 ;
then H2(D2, indx (D2,D1,j)) = H2(D2, indx (D2,D1,n1)) + (Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j))))) by A273, INTEGRA1:def 20;
then (H2(D1,n1) - H2(D2, indx (D2,D1,n1))) + ((Sum (mid (H1(D1),(n1 + 1),j))) - (Sum (mid (H1(D2),((indx (D2,D1,n1)) + 1),(indx (D2,D1,j)))))) = H2(D1,j) - H2(D2, indx (D2,D1,j)) by A272;
hence ex j being Element of NAT st
( j in dom D1 & D . (i + 1) in divset (D1,j) & H2(D1,j) - H2(D2, indx (D2,D1,j)) <= ((i + 1) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A232, A233, A551; :: thesis: verum
end;
hence S1[i + 1] ; :: thesis: verum
end;
for k being non empty Nat holds S1[k] from NAT_1:sch 10(A36, A227);
 then S1[i] ;
hence ex j being Element of NAT st
( j in dom D1 & D . i in divset (D1,j) & H2(D1,j) - H2(D2, indx (D2,D1,j)) <= (i * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A14; :: thesis: verum
end;
A553: len D1 in dom D1 by FINSEQ_5:6;
then D1 . (len D1) = D2 . (indx (D2,D1,(len D1))) by A10, INTEGRA1:def 19;
then upper_bound A = D2 . (indx (D2,D1,(len D1))) by INTEGRA1:def 2;
then A554: D2 . (len D2) = D2 . (indx (D2,D1,(len D1))) by INTEGRA1:def 2;
len D in dom D by FINSEQ_5:6;
then consider j being Element of NAT such that
A555: j in dom D1 and
A556: D . (len D) in divset (D1,j) and
A557: H2(D1,j) - H2(D2, indx (D2,D1,j)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A13;
A558: j = len D1
proof
j in Seg (len D1) by A555, FINSEQ_1:def 3;
then A559: j <= len D1 by FINSEQ_1:1;
assume j <> len D1 ; :: thesis: contradiction
then j < len D1 by A559, XXREAL_0:1;
then D1 . j < D1 . (len D1) by A555, A553, SEQM_3:def 1;
then A560: D1 . j < upper_bound A by INTEGRA1:def 2;
A561: upper_bound (divset (D1,j)) < upper_bound A D . (len D) <= upper_bound (divset (D1,j)) by A556, INTEGRA2:1;
hence contradiction by A561, INTEGRA1:def 2; :: thesis: verum
end;
indx (D2,D1,(len D1)) in dom D2 by A10, A553, INTEGRA1:def 19;
then indx (D2,D1,(len D1)) = len D2 by A12, A554, SEQ_4:138;
then (upper_sum (f,D1)) - H2(D2, len D2) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A557, A558, INTEGRA1:42;
hence (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by INTEGRA1:42; :: thesis: verum
end;
hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A9, A10, A11; :: thesis: verum
end;
hence ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) ; :: thesis: verum
end;
assume A562: delta T is convergent_to_0 ; :: thesis: ( not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
then A563: delta T is convergent by FDIFF_1:def 1;
A564: lim (delta T) = 0 by A562, FDIFF_1:def 1;
assume A565: vol A <> 0 ; :: thesis: ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
A566: delta T is non-empty by A562, FDIFF_1:def 1;
A567: for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )
proof
let e be Real; :: thesis: ( e > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e ) )
assume e > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )
then consider n being Element of NAT such that
A568: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < e by A563, A564, SEQ_2:def 7;
take n ; :: thesis: for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )
let m be Element of NAT ; :: thesis: ( n <= m implies ( 0 < (delta T) . m & (delta T) . m < e ) )
assume n <= m ; :: thesis: ( 0 < (delta T) . m & (delta T) . m < e )
then abs (((delta T) . m) - 0) < e by A568;
then A569: ((delta T) . m) + (abs (((delta T) . m) - 0)) < e + (abs (((delta T) . m) - 0)) by ABSVALUE:4, XREAL_1:8;
reconsider D = T . m as Division of A ;
A570: (delta T) . m = delta (T . m) by Def2;
delta (T . m) in rng (upper_volume ((chi (A,A)),(T . m))) by XXREAL_2:def 8;
then consider i being Element of NAT such that
A571: i in dom (upper_volume ((chi (A,A)),(T . m))) and
A572: delta (T . m) = (upper_volume ((chi (A,A)),(T . m))) . i by PARTFUN1:3;
i in Seg (len (upper_volume ((chi (A,A)),(T . m)))) by A571, FINSEQ_1:def 3;
then i in Seg (len D) by INTEGRA1:def 6;
then i in dom D by FINSEQ_1:def 3;
then A573: delta (T . m) = vol (divset ((T . m),i)) by A572, INTEGRA1:20;
(delta T) . m <> 0 by A566, SEQ_1:5;
hence ( 0 < (delta T) . m & (delta T) . m < e ) by A569, A570, A573, INTEGRA1:9, XREAL_1:6; :: thesis: verum
end;
A574: for e being real number st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e
proof
let e be real number ; :: thesis: ( e > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e )
assume A576: e > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e
then A577: e / 2 > 0 by XREAL_1:139;
reconsider e = e as Real by XREAL_0:def 1;
A578: rng (upper_sum_set f) is bounded_below by A1, INTEGRA2:35;
upper_integral f = lower_bound (rng (upper_sum_set f)) by INTEGRA1:def 14;
then consider y being real number such that
A579: y in rng (upper_sum_set f) and
A580: (upper_integral f) + (e / 2) > y by A577, A578, SEQ_4:def 2;
ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )
proof
consider D3 being Element of divs A such that
A581: D3 in dom (upper_sum_set f) and
A582: y = (upper_sum_set f) . D3 by A579, PARTFUN1:3;
reconsider D3 = D3 as Division of A by INTEGRA1:def 3;
A583: len D3 in Seg (len D3) by FINSEQ_1:3;
then 1 <= len D3 by FINSEQ_1:1;
then 1 in Seg (len D3) by FINSEQ_1:1;
then A584: 1 in dom D3 by FINSEQ_1:def 3;
per cases ( D3 . 1 <> lower_bound A or D3 . 1 = lower_bound A ) ;
suppose A586: D3 . 1 = lower_bound A ; :: thesis: ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )
ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )
proof
A587: (upper_volume (f,D3)) . 1 = (upper_bound (rng (f | (divset (D3,1))))) * (vol (divset (D3,1))) by A584, INTEGRA1:def 6;
vol A >= 0 by INTEGRA1:9;
then A588: (upper_bound A) - (lower_bound A) > 0 by A565, INTEGRA1:def 5;
A589: y = upper_sum (f,D3) by A582, INTEGRA1:def 10
.= Sum (upper_volume (f,D3)) by INTEGRA1:def 8
.= Sum (((upper_volume (f,D3)) | 1) ^ ((upper_volume (f,D3)) /^ 1)) by RFINSEQ:8 ;
A590: D3 . (len D3) = upper_bound A by INTEGRA1:def 2;
len D3 in dom D3 by A583, FINSEQ_1:def 3;
then A591: len D3 > 1 by A584, A586, A590, A588, SEQ_4:137, XREAL_1:47;
then reconsider D = D3 /^ 1 as increasing FinSequence of REAL by INTEGRA1:34;
A592: len D = (len D3) - 1 by A591, RFINSEQ:def 1;
upper_bound A > lower_bound A by A588, XREAL_1:47;
then len D <> 0 by A586, A592, INTEGRA1:def 2;
then reconsider D = D as non empty increasing FinSequence of REAL ;
A593: len D in dom D by FINSEQ_5:6;
(len D) + 1 = len D3 by A592;
then A594: D . (len D) = upper_bound A by A590, A591, A593, RFINSEQ:def 1;
A595: len D in Seg (len D) by FINSEQ_1:3;
1 + 1 <= len D3 by A591, NAT_1:13;
then 2 in dom D3 by FINSEQ_3:25;
then A596: D3 . 1 < D3 . 2 by A584, SEQM_3:def 1;
A597: rng D3 c= A by INTEGRA1:def 2;
rng D c= rng D3 by FINSEQ_5:33;
then rng D c= A by A597, XBOOLE_1:1;
then reconsider D = D as Division of A by A594, INTEGRA1:def 2;
A598: 1 in Seg 1 by FINSEQ_1:1;
A599: len D3 >= 1 + 1 by A591, NAT_1:13;
then A600: 2 <= len (upper_volume (f,D3)) by INTEGRA1:def 6;
1 <= len (upper_volume (f,D3)) by A591, INTEGRA1:def 6;
then A601: len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = ((len (upper_volume (f,D3))) -' 2) + 1 by A600, FINSEQ_6:118
.= ((len D3) -' 2) + 1 by INTEGRA1:def 6
.= ((len D3) - 2) + 1 by A599, XREAL_1:233
.= (len D3) - 1 ;
A602: for i being Nat st 1 <= i & i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) holds
(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) implies (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i )
assume that
A603: 1 <= i and
A604: i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) ; :: thesis: (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i
A605: 1 <= i + 1 by NAT_1:12;
i + 1 <= len D3 by A601, A604, XREAL_1:19;
then A606: i + 1 in Seg (len D3) by A605, FINSEQ_1:1;
then A607: i + 1 in dom D3 by FINSEQ_1:def 3;
A608: divset (D3,(i + 1)) = divset (D,i)
proof
A609: i + 1 in dom D3 by A606, FINSEQ_1:def 3;
A610: 1 <> i + 1 by A603, NAT_1:13;
then A611: upper_bound (divset (D3,(i + 1))) = D3 . (i + 1) by A609, INTEGRA1:def 4;
A612: i in dom D by A592, A601, A603, A604, FINSEQ_3:25;
then A613: D . i = D3 . (i + 1) by A591, RFINSEQ:def 1;
A614: lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1) by A610, A609, INTEGRA1:def 4;
per cases ( i = 1 or i <> 1 ) ;
suppose A618: i <> 1 ; :: thesis: divset (D3,(i + 1)) = divset (D,i)
then i - 1 in dom D by A612, INTEGRA1:7;
then A619: D . (i - 1) = D3 . ((i - 1) + 1) by A591, RFINSEQ:def 1
.= D3 . i ;
A620: upper_bound (divset (D,i)) = D . i by A612, A618, INTEGRA1:def 4;
lower_bound (divset (D,i)) = D . (i - 1) by A612, A618, INTEGRA1:def 4;
then divset (D3,(i + 1)) = [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).] by A611, A614, A613, A620, A619, INTEGRA1:4;
hence divset (D3,(i + 1)) = divset (D,i) by INTEGRA1:4; :: thesis: verum
end;
end;
end;
i <= (len (upper_volume (f,D3))) - 1 by A601, A604, INTEGRA1:def 6;
then A621: i <= ((len (upper_volume (f,D3))) - 2) + 1 ;
i in NAT by ORDINAL1:def 12;
then (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D3)) . ((i + 2) - 1) by A600, A603, A621, FINSEQ_6:122
.= (upper_volume (f,D3)) . (i + 1) ;
then A622: (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_bound (rng (f | (divset (D3,(i + 1)))))) * (vol (divset (D3,(i + 1)))) by A607, INTEGRA1:def 6;
i in Seg (len D) by A592, A601, A603, A604, FINSEQ_1:1;
then i in dom D by FINSEQ_1:def 3;
hence (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i by A622, A608, INTEGRA1:def 6; :: thesis: verum
end;
A623: 1 <= len (upper_volume (f,D3)) by A591, INTEGRA1:def 6;
then A624: len ((upper_volume (f,D3)) | 1) = 1 by FINSEQ_1:59;
1 in dom (upper_volume (f,D3)) by A623, FINSEQ_3:25;
then ((upper_volume (f,D3)) | 1) . 1 = (upper_volume (f,D3)) . 1 by A598, RFINSEQ:6;
then A625: (upper_volume (f,D3)) | 1 = <*((upper_volume (f,D3)) . 1)*> by A624, FINSEQ_1:40;
A626: 2 -' 1 = 2 - 1 by XREAL_1:233
.= 1 ;
1 <= len D by A595, FINSEQ_1:1;
then 1 in dom D by FINSEQ_3:25;
then A627: D . 1 = D3 . (1 + 1) by A591, RFINSEQ:def 1
.= D3 . 2 ;
D in divs A by INTEGRA1:def 3;
then A628: D in dom (upper_sum_set f) by FUNCT_2:def 1;
len (upper_volume (f,D3)) >= 2 by A599, INTEGRA1:def 6;
then A629: mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3)))) = (upper_volume (f,D3)) /^ 1 by A626, FINSEQ_6:117;
len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = len (upper_volume (f,D)) by A592, A601, INTEGRA1:def 6;
then A630: (upper_volume (f,D3)) /^ 1 = upper_volume (f,D) by A629, A602, FINSEQ_1:14;
vol (divset (D3,1)) = (upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1))) by INTEGRA1:def 5
.= (upper_bound (divset (D3,1))) - (lower_bound A) by A584, INTEGRA1:def 4
.= (D3 . 1) - (lower_bound A) by A584, INTEGRA1:def 4
.= 0 by A586 ;
then y = 0 + (Sum (upper_volume (f,D))) by A589, A625, A587, A630, RVSUM_1:76
.= upper_sum (f,D) by INTEGRA1:def 8 ;
then y = (upper_sum_set f) . D by INTEGRA1:def 10;
hence ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) by A586, A628, A627, A596; :: thesis: verum
end;
hence ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A ) ; :: thesis: verum
end;
end;
end;
then consider D being Division of A such that
D in dom (upper_sum_set f) and
A632: y = (upper_sum_set f) . D and
A633: D . 1 > lower_bound A ;
deffunc H1( Nat) -> Element of REAL = vol (divset (D,$1));
set p = len D;
set H = upper_bound (rng f);
set h = lower_bound (rng f);
consider v being FinSequence of REAL such that
A634: ( len v = len D & ( for j being Nat st j in dom v holds
v . j = H1(j) ) ) from FINSEQ_2:sch 1();
 A635: 2 * (len D) > 0 by XREAL_1:129;
consider v1 being non-decreasing FinSequence of REAL such that
A636: v,v1 are_fiberwise_equipotent by INTEGRA2:3;
defpred S1[ Nat] means ( $1 in dom v1 & v1 . $1 > 0 );
A637: dom v = Seg (len D) by A634, FINSEQ_1:def 3;
A638: ex k being Nat st S1[k]
proof
consider H being Function such that
dom H = dom v and
rng H = dom v1 and
H is one-to-one and
A639: v = v1 * H by A636, CLASSES1:77;
consider k being Element of NAT such that
A640: k in dom D and
A641: vol (divset (D,k)) > 0 by A565, Th2;
A642: dom D = Seg (len D) by FINSEQ_1:def 3;
then H . k in dom v1 by A637, A639, A640, FUNCT_1:11;
then reconsider Hk = H . k as Element of NAT ;
v . k > 0 by A634, A637, A640, A641, A642;
then S1[Hk] by A637, A639, A640, A642, FUNCT_1:11, FUNCT_1:12;
hence ex k being Nat st S1[k] ; :: thesis: verum
end;
consider k being Nat such that
A643: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch 5(A638);
 A644: (upper_bound (rng f)) - (lower_bound (rng f)) >= 0 by A1, Lm3, XREAL_1:48;
then A645: (2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0 by A635, XREAL_1:129;
min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0
proof
per cases ( min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = v1 . k or min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) ) by XXREAL_0:15;
suppose min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = v1 . k ; :: thesis: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0
hence min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0 by A643; :: thesis: verum
end;
suppose min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) = e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) ; :: thesis: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0
hence min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) > 0 by A576, A645, XREAL_1:139; :: thesis: verum
end;
end;
end;
then consider n being Element of NAT such that
A646: for m being Element of NAT st n <= m holds
( 0 < (delta T) . m & (delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) ) by A567;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e
A647: y = upper_sum (f,D) by A632, INTEGRA1:def 10;
for m being Element of NAT st n <= m holds
abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e
proof
A648: v1 . 1 > 0
proof
A649: for n1 being Element of NAT st n1 in dom D holds
vol (divset (D,n1)) > 0
proof
let n1 be Element of NAT ; :: thesis: ( n1 in dom D implies vol (divset (D,n1)) > 0 )
assume A650: n1 in dom D ; :: thesis: vol (divset (D,n1)) > 0
then A651: 1 <= n1 by FINSEQ_3:25;
per cases ( n1 = 1 or n1 > 1 ) by A651, XXREAL_0:1;
suppose A654: n1 > 1 ; :: thesis: vol (divset (D,n1)) > 0
then A655: upper_bound (divset (D,n1)) = D . n1 by A650, INTEGRA1:def 4;
lower_bound (divset (D,n1)) = D . (n1 - 1) by A650, A654, INTEGRA1:def 4;
then A656: vol (divset (D,n1)) = (D . n1) - (D . (n1 - 1)) by A655, INTEGRA1:def 5;
n1 < n1 + 1 by XREAL_1:29;
then A657: n1 - 1 < n1 by XREAL_1:19;
n1 - 1 in dom D by A650, A654, INTEGRA1:7;
then D . (n1 - 1) < D . n1 by A650, A657, SEQM_3:def 1;
hence vol (divset (D,n1)) > 0 by A656, XREAL_1:50; :: thesis: verum
end;
end;
end;
A658: k <= len v1 by A643, FINSEQ_3:25;
1 <= k by A643, FINSEQ_3:25;
then 1 <= len v1 by A658, XXREAL_0:2;
then 1 in dom v1 by FINSEQ_3:25;
then A659: v1 . 1 in rng v1 by FUNCT_1:def 3;
rng v = rng v1 by A636, CLASSES1:75;
then consider n1 being Element of NAT such that
A660: n1 in dom v and
A661: v1 . 1 = v . n1 by A659, PARTFUN1:3;
n1 in Seg (len D) by A634, A660, FINSEQ_1:def 3;
then A662: n1 in dom D by FINSEQ_1:def 3;
v1 . 1 = vol (divset (D,n1)) by A634, A660, A661;
hence v1 . 1 > 0 by A649, A662; :: thesis: verum
end;
A663: v1 . k = min (rng (upper_volume ((chi (A,A)),D)))
proof
A664: k = 1 A667: rng v = rng v1 by A636, CLASSES1:75;
v1 . k in rng (upper_volume ((chi (A,A)),D))
proof
v1 . k in rng v by A643, A667, FUNCT_1:def 3;
then consider k2 being Element of NAT such that
A668: k2 in dom v and
A669: v1 . k = v . k2 by PARTFUN1:3;
A670: k2 in Seg (len D) by A634, A668, FINSEQ_1:def 3;
then A671: k2 in dom D by FINSEQ_1:def 3;
k2 in Seg (len (upper_volume ((chi (A,A)),D))) by A670, INTEGRA1:def 6;
then A672: k2 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
v1 . k = vol (divset (D,k2)) by A634, A668, A669;
then v1 . k = (upper_volume ((chi (A,A)),D)) . k2 by A671, INTEGRA1:20;
hence v1 . k in rng (upper_volume ((chi (A,A)),D)) by A672, FUNCT_1:def 3; :: thesis: verum
end;
then A673: v1 . k >= min (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def 7;
min (rng (upper_volume ((chi (A,A)),D))) in rng (upper_volume ((chi (A,A)),D)) by XXREAL_2:def 7;
then consider m being Element of NAT such that
A674: m in dom (upper_volume ((chi (A,A)),D)) and
A675: min (rng (upper_volume ((chi (A,A)),D))) = (upper_volume ((chi (A,A)),D)) . m by PARTFUN1:3;
m in Seg (len (upper_volume ((chi (A,A)),D))) by A674, FINSEQ_1:def 3;
then A676: m in Seg (len D) by INTEGRA1:def 6;
then m in dom D by FINSEQ_1:def 3;
then min (rng (upper_volume ((chi (A,A)),D))) = vol (divset (D,m)) by A675, INTEGRA1:20;
then A677: v . m = min (rng (upper_volume ((chi (A,A)),D))) by A634, A637, A676;
m in dom v by A634, A676, FINSEQ_1:def 3;
then min (rng (upper_volume ((chi (A,A)),D))) in rng v by A677, FUNCT_1:def 3;
then consider m1 being Element of NAT such that
A678: m1 in dom v1 and
A679: min (rng (upper_volume ((chi (A,A)),D))) = v1 . m1 by A667, PARTFUN1:3;
m1 >= 1 by A678, FINSEQ_3:25;
then v1 . 1 <= min (rng (upper_volume ((chi (A,A)),D))) by A643, A664, A678, A679, INTEGRA2:2;
hence v1 . k = min (rng (upper_volume ((chi (A,A)),D))) by A664, A673, XXREAL_0:1; :: thesis: verum
end;
A680: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) <= v1 . k by XXREAL_0:17;
set s = upper_integral f;
set sD = upper_sum (f,D);
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e )
reconsider D1 = T . m as Division of A ;
A681: delta D1 = (delta T) . m by Def2;
consider D2 being Division of A such that
A682: D <= D2 and
D1 <= D2 and
A683: 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;
set sD1 = upper_sum (f,(T . m));
set sD2 = upper_sum (f,D2);
upper_sum (f,D2) <= upper_sum (f,D) by A1, A682, INTEGRA1:45;
then A684: (upper_sum (f,(T . m))) - (upper_sum (f,D)) <= (upper_sum (f,(T . m))) - (upper_sum (f,D2)) by XREAL_1:10;
(((upper_sum (f,D)) + (upper_sum (f,(T . m)))) - (upper_sum (f,(T . m)))) - (upper_integral f) < e / 2 by A580, A647, XREAL_1:19;
then (((upper_sum (f,(T . m))) - (upper_integral f)) + (upper_sum (f,D))) - (upper_sum (f,(T . m))) < e / 2 ;
then ((upper_sum (f,(T . m))) - (upper_integral f)) + (upper_sum (f,D)) < (upper_sum (f,(T . m))) + (e / 2) by XREAL_1:19;
then A685: (upper_sum (f,(T . m))) - (upper_integral f) < ((upper_sum (f,(T . m))) + (e / 2)) - (upper_sum (f,D)) by XREAL_1:20;
T . m in divs A by INTEGRA1:def 3;
then A686: T . m in dom (upper_sum_set f) by FUNCT_2:def 1;
(upper_sum (f,T)) . m = upper_sum (f,(T . m)) by INTEGRA2:def 2;
then (upper_sum (f,T)) . m = (upper_sum_set f) . (T . m) by INTEGRA1:def 10;
then (upper_sum (f,T)) . m in rng (upper_sum_set f) by A686, FUNCT_1:def 3;
then lower_bound (rng (upper_sum_set f)) <= (upper_sum (f,T)) . m by A578, SEQ_4:def 2;
then upper_integral f <= (upper_sum (f,T)) . m by INTEGRA1:def 14;
then A687: ((upper_sum (f,T)) . m) - (upper_integral f) >= 0 by XREAL_1:48;
(upper_bound (rng f)) - (lower_bound (rng f)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) + 1 by XREAL_1:29;
then A688: (len D) * ((upper_bound (rng f)) - (lower_bound (rng f))) <= (len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) by XREAL_1:64;
A689: min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) <= e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by XXREAL_0:17;
assume A690: n <= m ; :: thesis: abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e
then (delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by A646;
then (delta T) . m < e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) by A689, XXREAL_0:2;
then ((delta T) . m) * ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) < e by A635, A644, XREAL_1:79, XREAL_1:129;
then (((delta T) . m) * ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) * 2 < e ;
then A691: ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) < e / 2 by XREAL_1:81;
(delta T) . m < min ((v1 . k),(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) by A646, A690;
then delta D1 < v1 . k by A681, A680, XXREAL_0:2;
then ex D3 being Division of A st
( D <= D3 & D1 <= D3 & rng D3 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D3)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) ) by A7, A663;
then A692: (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) by A683, Th6;
0 < (delta T) . m by A646, A690;
then ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * ((delta T) . m) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A688, XREAL_1:64;
then (upper_sum (f,(T . m))) - (upper_sum (f,D2)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A681, A692, XXREAL_0:2;
then (upper_sum (f,(T . m))) - (upper_sum (f,D)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) by A684, XXREAL_0:2;
then (upper_sum (f,(T . m))) - (upper_sum (f,D)) < e / 2 by A691, XXREAL_0:2;
then ((upper_sum (f,(T . m))) - (upper_sum (f,D))) + (e / 2) < (e / 2) + (e / 2) by XREAL_1:6;
then (upper_sum (f,(T . m))) - (upper_integral f) < e by A685, XXREAL_0:2;
then ((upper_sum (f,T)) . m) - (upper_integral f) < e by INTEGRA2:def 2;
hence abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e by A687, ABSVALUE:def 1; :: thesis: verum
end;
hence for m being Element of NAT st n <= m holds
abs (((upper_sum (f,T)) . m) - (upper_integral f)) < e ; :: thesis: verum
end;
hence upper_sum (f,T) is convergent by SEQ_2:def 6; :: thesis: lim (upper_sum (f,T)) = upper_integral f
hence lim (upper_sum (f,T)) = upper_integral f by A574, SEQ_2:def 7; :: thesis: verum