let A be closed-interval Subset of REAL; :: thesis: for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds
for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i)))
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds
for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i)))
let f be Function of A,REAL; :: thesis: ( D1 <= D2 & f | A is bounded_below implies for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i))) )
assume that
A1: D1 <= D2 and
A2: f | A is bounded_below ; :: thesis: for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i)))
for i being non empty Nat st i in dom D1 holds
Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i)))
proof
defpred S1[ Nat] means ( $1 in dom D1 implies Sum ((lower_volume (f,D1)) | $1) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,$1))) );
A3: S1[1]
proof
set g = f | (divset (D1,1));
set B = divset (D1,1);
set DD2 = mid (D2,1,(indx (D2,D1,1)));
set DD1 = mid (D1,1,1);
reconsider g = f | (divset (D1,1)) as PartFunc of (divset (D1,1)),REAL by PARTFUN1:43;
A4: dom g = (dom f) /\ (divset (D1,1)) by RELAT_1:90;
assume A5: 1 in dom D1 ; :: thesis: Sum ((lower_volume (f,D1)) | 1) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,1)))
then A6: D1 . 1 = upper_bound (divset (D1,1)) by Def5;
then A7: D2 . (indx (D2,D1,1)) = upper_bound (divset (D1,1)) by A1, A5, Def21;
lower_bound (divset (D1,1)) <= upper_bound (divset (D1,1)) by SEQ_4:24;
then reconsider DD1 = mid (D1,1,1) as Division of divset (D1,1) by A5, A6, Th39;
1 in Seg (len D1) by A5, FINSEQ_1:def 3;
then A8: 1 <= len D1 by FINSEQ_1:3;
then A9: len (mid (D1,1,1)) = (1 -' 1) + 1 by FINSEQ_6:124;
A10: len (lower_volume (g,DD1)) = len DD1 by Def8
.= 1 by A9, XREAL_1:237 ;
A11: len (mid (D1,1,1)) = 1 by A9, XREAL_1:237;
then A12: len (mid (D1,1,1)) = len (D1 | 1) by A8, FINSEQ_1:80;
for k being Nat st 1 <= k & k <= len (mid (D1,1,1)) holds
(mid (D1,1,1)) . k = (D1 | 1) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len (mid (D1,1,1)) implies (mid (D1,1,1)) . k = (D1 | 1) . k )
assume that
A13: 1 <= k and
A14: k <= len (mid (D1,1,1)) ; :: thesis: (mid (D1,1,1)) . k = (D1 | 1) . k
k in Seg (len (D1 | 1)) by A12, A13, A14, FINSEQ_1:3;
then k in dom (D1 | 1) by FINSEQ_1:def 3;
then k in dom (D1 | (Seg 1)) by FINSEQ_1:def 15;
then A15: (D1 | (Seg 1)) . k = D1 . k by FUNCT_1:70;
A16: k = 1 by A11, A13, A14, XXREAL_0:1;
then (mid (D1,1,1)) . k = D1 . ((1 + 1) - 1) by A8, FINSEQ_6:124;
hence (mid (D1,1,1)) . k = (D1 | 1) . k by A16, A15, FINSEQ_1:def 15; :: thesis: verum
end;
then A17: mid (D1,1,1) = D1 | 1 by A12, FINSEQ_1:18;
A18: for i being Nat st 1 <= i & i <= len (lower_volume (g,DD1)) holds
(lower_volume (g,DD1)) . i = ((lower_volume (f,D1)) | 1) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume (g,DD1)) implies (lower_volume (g,DD1)) . i = ((lower_volume (f,D1)) | 1) . i )
assume that
A19: 1 <= i and
A20: i <= len (lower_volume (g,DD1)) ; :: thesis: (lower_volume (g,DD1)) . i = ((lower_volume (f,D1)) | 1) . i
A21: 1 in Seg 1 by FINSEQ_1:5;
dom (D1 | (Seg 1)) = (dom D1) /\ (Seg 1) by RELAT_1:90;
then A22: 1 in dom (D1 | (Seg 1)) by A5, A21, XBOOLE_0:def 4;
dom (lower_volume (f,D1)) = Seg (len (lower_volume (f,D1))) by FINSEQ_1:def 3
.= Seg (len D1) by Def8 ;
then A23: dom ((lower_volume (f,D1)) | (Seg 1)) = (Seg (len D1)) /\ (Seg 1) by RELAT_1:90
.= Seg 1 by A8, FINSEQ_1:9 ;
len DD1 = 1 by A9, XREAL_1:237;
then A24: 1 in dom DD1 by A21, FINSEQ_1:def 3;
A25: ((lower_volume (f,D1)) | 1) . i = ((lower_volume (f,D1)) | (Seg 1)) . i by FINSEQ_1:def 15
.= ((lower_volume (f,D1)) | (Seg 1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (lower_volume (f,D1)) . 1 by A23, FINSEQ_1:5, FUNCT_1:70
.= (lower_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) by A5, Def8 ;
A26: divset (D1,1) = [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by Th5
.= [.(lower_bound A),(upper_bound (divset (D1,1))).] by A5, Def5
.= [.(lower_bound A),(D1 . 1).] by A5, Def5 ;
A27: (lower_volume (g,DD1)) . i = (lower_volume (g,DD1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (lower_bound (rng (g | (divset (DD1,1))))) * (vol (divset (DD1,1))) by A24, Def8 ;
divset (DD1,1) = [.(lower_bound (divset (DD1,1))),(upper_bound (divset (DD1,1))).] by Th5
.= [.(lower_bound (divset (D1,1))),(upper_bound (divset (DD1,1))).] by A24, Def5
.= [.(lower_bound (divset (D1,1))),(DD1 . 1).] by A24, Def5
.= [.(lower_bound A),((D1 | 1) . 1).] by A5, A17, Def5
.= [.(lower_bound A),((D1 | (Seg 1)) . 1).] by FINSEQ_1:def 15
.= [.(lower_bound A),(D1 . 1).] by A22, FUNCT_1:70 ;
hence (lower_volume (g,DD1)) . i = ((lower_volume (f,D1)) | 1) . i by A4, A27, A26, A25, RELAT_1:97; :: thesis: verum
end;
A28: g | (divset (D1,1)) is bounded_below
proof
consider a being real number such that
A29: for x being set st x in A /\ (dom f) holds
a <= f . x by A2, RFUNCT_1:88;
for x being set st x in (divset (D1,1)) /\ (dom g) holds
a <= g . x
proof
let x be set ; :: thesis: ( x in (divset (D1,1)) /\ (dom g) implies a <= g . x )
A30: dom g c= dom f by RELAT_1:89;
assume x in (divset (D1,1)) /\ (dom g) ; :: thesis: a <= g . x
then A31: x in dom g by XBOOLE_0:def 4;
A32: A /\ (dom f) = dom f by XBOOLE_1:28;
then reconsider x = x as Element of A by A31, A30, XBOOLE_0:def 4;
a <= f . x by A29, A31, A32, A30;
hence a <= g . x by A31, FUNCT_1:70; :: thesis: verum
end;
hence g | (divset (D1,1)) is bounded_below by RFUNCT_1:88; :: thesis: verum
end;
A33: rng D2 c= A by Def2;
A34: indx (D2,D1,1) in dom D2 by A1, A5, Def21;
then A35: indx (D2,D1,1) in Seg (len D2) by FINSEQ_1:def 3;
then A36: 1 <= indx (D2,D1,1) by FINSEQ_1:3;
A37: indx (D2,D1,1) <= len D2 by A35, FINSEQ_1:3;
then 1 <= len D2 by A36, XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:3;
then A38: 1 in dom D2 by FINSEQ_1:def 3;
then D2 . 1 in rng D2 by FUNCT_1:def 5;
then D2 . 1 in A by A33;
then D2 . 1 in [.(lower_bound A),(upper_bound A).] by Th5;
then D2 . 1 in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by RCOMP_1:def 1;
then ex a being Real st
( D2 . 1 = a & lower_bound A <= a & a <= upper_bound A ) ;
then D2 . 1 >= lower_bound (divset (D1,1)) by A5, Def5;
then reconsider DD2 = mid (D2,1,(indx (D2,D1,1))) as Division of divset (D1,1) by A34, A36, A38, A7, Th39;
indx (D2,D1,1) in dom D2 by A1, A5, Def21;
then A39: indx (D2,D1,1) in Seg (len D2) by FINSEQ_1:def 3;
then A40: 1 <= indx (D2,D1,1) by FINSEQ_1:3;
A41: indx (D2,D1,1) <= len D2 by A39, FINSEQ_1:3;
then A42: 1 <= len D2 by A40, XXREAL_0:2;
then len (mid (D2,1,(indx (D2,D1,1)))) = ((indx (D2,D1,1)) -' 1) + 1 by A40, A41, FINSEQ_6:124;
then A43: len (mid (D2,1,(indx (D2,D1,1)))) = ((indx (D2,D1,1)) - 1) + 1 by A40, XREAL_1:235;
then A44: len (mid (D2,1,(indx (D2,D1,1)))) = len (D2 | (indx (D2,D1,1))) by A41, FINSEQ_1:80;
A45: for k being Nat st 1 <= k & k <= len (mid (D2,1,(indx (D2,D1,1)))) holds
(mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len (mid (D2,1,(indx (D2,D1,1)))) implies (mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k )
assume that
A46: 1 <= k and
A47: k <= len (mid (D2,1,(indx (D2,D1,1)))) ; :: thesis: (mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k
A48: k in Seg (len (D2 | (indx (D2,D1,1)))) by A44, A46, A47, FINSEQ_1:3;
then k in dom (D2 | (indx (D2,D1,1))) by FINSEQ_1:def 3;
then k in dom (D2 | (Seg (indx (D2,D1,1)))) by FINSEQ_1:def 15;
then A49: (D2 | (Seg (indx (D2,D1,1)))) . k = D2 . k by FUNCT_1:70;
(mid (D2,1,(indx (D2,D1,1)))) . k = D2 . ((k + 1) -' 1) by A40, A41, A42, A46, A47, A48, FINSEQ_6:124;
then (mid (D2,1,(indx (D2,D1,1)))) . k = D2 . ((k + 1) - 1) by NAT_1:11, XREAL_1:235;
hence (mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k by A49, FINSEQ_1:def 15; :: thesis: verum
end;
then A50: mid (D2,1,(indx (D2,D1,1))) = D2 | (indx (D2,D1,1)) by A44, FINSEQ_1:18;
A51: for i being Nat st 1 <= i & i <= len (lower_volume (g,DD2)) holds
(lower_volume (g,DD2)) . i = ((lower_volume (f,D2)) | (indx (D2,D1,1))) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume (g,DD2)) implies (lower_volume (g,DD2)) . i = ((lower_volume (f,D2)) | (indx (D2,D1,1))) . i )
assume that
A52: 1 <= i and
A53: i <= len (lower_volume (g,DD2)) ; :: thesis: (lower_volume (g,DD2)) . i = ((lower_volume (f,D2)) | (indx (D2,D1,1))) . i
A54: i <= len DD2 by A53, Def8;
then A55: i in Seg (len DD2) by A52, FINSEQ_1:3;
then A56: i in dom DD2 by FINSEQ_1:def 3;
divset (DD2,i) = divset (D2,i)
proof
Seg (indx (D2,D1,1)) c= Seg (len D2) by A41, FINSEQ_1:7;
then i in Seg (len D2) by A43, A55;
then A57: i in dom D2 by FINSEQ_1:def 3;
now
per cases ( i = 1 or i <> 1 ) ;
suppose A58: i = 1 ; :: thesis: divset (DD2,i) = divset (D2,i)
then A59: 1 in dom (D2 | (Seg (indx (D2,D1,1)))) by A50, A56, FINSEQ_1:def 15;
then 1 in (dom D2) /\ (Seg (indx (D2,D1,1))) by RELAT_1:90;
then A60: 1 in dom D2 by XBOOLE_0:def 4;
A61: divset (D2,i) = [.(lower_bound (divset (D2,1))),(upper_bound (divset (D2,1))).] by A58, Th5
.= [.(lower_bound A),(upper_bound (divset (D2,1))).] by A60, Def5
.= [.(lower_bound A),(D2 . 1).] by A60, Def5 ;
divset (DD2,i) = [.(lower_bound (divset (DD2,1))),(upper_bound (divset (DD2,1))).] by A58, Th5
.= [.(lower_bound (divset (D1,1))),(upper_bound (divset (DD2,1))).] by A56, A58, Def5
.= [.(lower_bound (divset (D1,1))),(DD2 . 1).] by A56, A58, Def5
.= [.(lower_bound (divset (D1,1))),((D2 | (indx (D2,D1,1))) . 1).] by A45, A54, A58
.= [.(lower_bound (divset (D1,1))),((D2 | (Seg (indx (D2,D1,1)))) . 1).] by FINSEQ_1:def 15
.= [.(lower_bound (divset (D1,1))),(D2 . 1).] by A59, FUNCT_1:70
.= [.(lower_bound A),(D2 . 1).] by A5, Def5 ;
hence divset (DD2,i) = divset (D2,i) by A61; :: thesis: verum
end;
suppose A62: i <> 1 ; :: thesis: divset (DD2,i) = divset (D2,i)
A63: i - 1 in dom (D2 | (Seg (indx (D2,D1,1)))) DD2 . (i - 1) = (D2 | (indx (D2,D1,1))) . (i - 1) by A44, A45, FINSEQ_1:18
.= (D2 | (Seg (indx (D2,D1,1)))) . (i - 1) by FINSEQ_1:def 15 ;
then A69: DD2 . (i - 1) = D2 . (i - 1) by A63, FUNCT_1:70;
i <= len D2 by A43, A37, A54, XXREAL_0:2;
then i in Seg (len D2) by A52, FINSEQ_1:3;
then i in dom D2 by FINSEQ_1:def 3;
then i in (dom D2) /\ (Seg (indx (D2,D1,1))) by A43, A55, XBOOLE_0:def 4;
then A70: i in dom (D2 | (Seg (indx (D2,D1,1)))) by RELAT_1:90;
DD2 . i = (D2 | (indx (D2,D1,1))) . i by A44, A45, FINSEQ_1:18
.= (D2 | (Seg (indx (D2,D1,1)))) . i by FINSEQ_1:def 15 ;
then A71: DD2 . i = D2 . i by A70, FUNCT_1:70;
A72: divset (D2,i) = [.(lower_bound (divset (D2,i))),(upper_bound (divset (D2,i))).] by Th5
.= [.(D2 . (i - 1)),(upper_bound (divset (D2,i))).] by A57, A62, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A57, A62, Def5 ;
divset (DD2,i) = [.(lower_bound (divset (DD2,i))),(upper_bound (divset (DD2,i))).] by Th5
.= [.(DD2 . (i - 1)),(upper_bound (divset (DD2,i))).] by A56, A62, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A56, A62, A69, A71, Def5 ;
hence divset (DD2,i) = divset (D2,i) by A72; :: thesis: verum
end;
end;
end;
hence divset (DD2,i) = divset (D2,i) ; :: thesis: verum
end;
then A73: (lower_volume (g,DD2)) . i = (lower_bound (rng (g | (divset (D2,i))))) * (vol (divset (D2,i))) by A56, Def8;
Seg (indx (D2,D1,1)) c= Seg (len D2) by A41, FINSEQ_1:7;
then i in Seg (len D2) by A43, A55;
then A74: i in dom D2 by FINSEQ_1:def 3;
A75: i in dom DD2 by A55, FINSEQ_1:def 3;
A76: now
per cases ( i = 1 or i <> 1 ) ;
suppose A77: i = 1 ; :: thesis: ( lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] & upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] )
then 1 in dom (D2 | (Seg (indx (D2,D1,1)))) by A50, A75, FINSEQ_1:def 15;
then 1 in (dom D2) /\ (Seg (indx (D2,D1,1))) by RELAT_1:90;
then A78: 1 in dom D2 by XBOOLE_0:def 4;
then D2 . 1 <= D2 . (indx (D2,D1,1)) by A34, A36, SEQ_4:154;
then A79: D2 . 1 <= D1 . 1 by A1, A5, Def21;
lower_bound (divset (D2,i)) = lower_bound A by A77, A78, Def5;
then A80: lower_bound (divset (D2,i)) = lower_bound (divset (D1,1)) by A5, Def5;
upper_bound (divset (D2,i)) = D2 . 1 by A77, A78, Def5;
then A81: upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A5, A79, Def5;
lower_bound (divset (D1,1)) <= upper_bound (divset (D1,1)) by Th4;
hence lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by A80, XXREAL_1:1; :: thesis: upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
lower_bound (divset (D2,i)) <= upper_bound (divset (D2,i)) by Th4;
then upper_bound (divset (D2,i)) in { r where r is Real : ( lower_bound (divset (D1,1)) <= r & r <= upper_bound (divset (D1,1)) ) } by A80, A81;
hence upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by RCOMP_1:def 1; :: thesis: verum
end;
suppose A82: i <> 1 ; :: thesis: ( lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] & upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] )
then not i is trivial by A52, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:31;
then A83: 1 <= i - 1 by XREAL_1:21;
A84: ex j being Nat st i = 1 + j by A52, NAT_1:10;
A85: rng D2 c= A by Def2;
A86: lower_bound (divset (D2,i)) = D2 . (i - 1) by A74, A82, Def5;
A87: lower_bound (divset (D1,1)) = lower_bound A by A5, Def5;
A88: i - 1 <= (indx (D2,D1,1)) - 0 by A43, A54, XREAL_1:15;
then i - 1 <= len D2 by A37, XXREAL_0:2;
then i - 1 in Seg (len D2) by A84, A83, FINSEQ_1:3;
then A89: i - 1 in dom D2 by FINSEQ_1:def 3;
then D2 . (i - 1) in rng D2 by FUNCT_1:def 5;
then A90: lower_bound (divset (D2,i)) >= lower_bound (divset (D1,1)) by A86, A87, A85, SEQ_4:def 5;
A91: upper_bound (divset (D1,1)) = D1 . 1 by A5, Def5;
D2 . (i - 1) <= D2 . (indx (D2,D1,1)) by A34, A88, A89, SEQ_4:154;
then lower_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A1, A5, A86, A91, Def21;
then lower_bound (divset (D2,i)) in { r where r is Real : ( lower_bound (divset (D1,1)) <= r & r <= upper_bound (divset (D1,1)) ) } by A90;
hence lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by RCOMP_1:def 1; :: thesis: upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).]
A92: upper_bound (divset (D2,i)) = D2 . i by A74, A82, Def5;
D2 . i in rng D2 by A74, FUNCT_1:def 5;
then A93: upper_bound (divset (D2,i)) >= lower_bound (divset (D1,1)) by A92, A87, A85, SEQ_4:def 5;
D2 . i <= D2 . (indx (D2,D1,1)) by A43, A34, A54, A74, SEQ_4:154;
then upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A1, A5, A92, A91, Def21;
then upper_bound (divset (D2,i)) in { r where r is Real : ( lower_bound (divset (D1,1)) <= r & r <= upper_bound (divset (D1,1)) ) } by A93;
hence upper_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by RCOMP_1:def 1; :: thesis: verum
end;
end;
end;
A94: divset (D1,1) = [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by Th5;
A95: Seg (indx (D2,D1,1)) c= Seg (len D2) by A41, FINSEQ_1:7;
then i in Seg (len D2) by A43, A55;
then A96: i in dom D2 by FINSEQ_1:def 3;
divset (D2,i) = [.(lower_bound (divset (D2,i))),(upper_bound (divset (D2,i))).] by Th5;
then A97: divset (D2,i) c= divset (D1,1) by A94, A76, XXREAL_2:def 12;
A98: dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,1)))) = (dom (lower_volume (f,D2))) /\ (Seg (indx (D2,D1,1))) by RELAT_1:90
.= (Seg (len (lower_volume (f,D2)))) /\ (Seg (indx (D2,D1,1))) by FINSEQ_1:def 3
.= (Seg (len D2)) /\ (Seg (indx (D2,D1,1))) by Def8
.= Seg (indx (D2,D1,1)) by A95, XBOOLE_1:28 ;
((lower_volume (f,D2)) | (indx (D2,D1,1))) . i = ((lower_volume (f,D2)) | (Seg (indx (D2,D1,1)))) . i by FINSEQ_1:def 15
.= (lower_volume (f,D2)) . i by A43, A55, A98, FUNCT_1:70
.= (lower_bound (rng (f | (divset (D2,i))))) * (vol (divset (D2,i))) by A96, Def8 ;
hence (lower_volume (g,DD2)) . i = ((lower_volume (f,D2)) | (indx (D2,D1,1))) . i by A73, A97, FUNCT_1:82; :: thesis: verum
end;
1 <= len (lower_volume (f,D1)) by A8, Def8;
then len (lower_volume (g,DD1)) = len ((lower_volume (f,D1)) | 1) by A10, FINSEQ_1:80;
then A99: lower_volume (g,DD1) = (lower_volume (f,D1)) | 1 by A18, FINSEQ_1:18;
A100: indx (D2,D1,1) <= len (lower_volume (f,D2)) by A41, Def8;
len (lower_volume (g,DD2)) = indx (D2,D1,1) by A43, Def8;
then A101: len (lower_volume (g,DD2)) = len ((lower_volume (f,D2)) | (indx (D2,D1,1))) by A100, FINSEQ_1:80;
dom g = A /\ (divset (D1,1)) by A4, FUNCT_2:def 1;
then dom g = divset (D1,1) by A5, Th10, XBOOLE_1:28;
then g is total by PARTFUN1:def 4;
then lower_sum (g,DD1) <= lower_sum (g,DD2) by A11, A28, Th33;
hence Sum ((lower_volume (f,D1)) | 1) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,1))) by A99, A101, A51, FINSEQ_1:18; :: thesis: verum
end;
A102: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A103: ( k in dom D1 implies Sum ((lower_volume (f,D1)) | k) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,k))) ) ; :: thesis: S1[k + 1]
assume A104: k + 1 in dom D1 ; :: thesis: Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))
then A105: k + 1 in Seg (len D1) by FINSEQ_1:def 3;
then A106: 1 <= k + 1 by FINSEQ_1:3;
A107: k + 1 <= len D1 by A105, FINSEQ_1:3;
now
per cases ( 1 = k + 1 or 1 <> k + 1 ) ;
suppose 1 = k + 1 ; :: thesis: Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))
hence Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A3, A104; :: thesis: verum
end;
suppose A108: 1 <> k + 1 ; :: thesis: Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))
set IDK = indx (D2,D1,k);
set IDK1 = indx (D2,D1,(k + 1));
set K1D2 = (lower_volume (f,D2)) | (indx (D2,D1,(k + 1)));
set KD1 = (lower_volume (f,D1)) | k;
set K1D1 = (lower_volume (f,D1)) | (k + 1);
set n = k + 1;
A109: k + 1 <= len (lower_volume (f,D1)) by A107, Def8;
then A110: len ((lower_volume (f,D1)) | (k + 1)) = k + 1 by FINSEQ_1:80;
then consider p1, q1 being FinSequence of REAL such that
A111: len p1 = k and
A112: len q1 = 1 and
A113: (lower_volume (f,D1)) | (k + 1) = p1 ^ q1 by FINSEQ_2:26;
A114: k <= k + 1 by NAT_1:11;
then A115: k <= len D1 by A107, XXREAL_0:2;
then A116: k <= len (lower_volume (f,D1)) by Def8;
then A117: len p1 = len ((lower_volume (f,D1)) | k) by A111, FINSEQ_1:80;
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = ((lower_volume (f,D1)) | k) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len p1 implies p1 . i = ((lower_volume (f,D1)) | k) . i )
assume that
A118: 1 <= i and
A119: i <= len p1 ; :: thesis: p1 . i = ((lower_volume (f,D1)) | k) . i
A120: i in Seg (len p1) by A118, A119, FINSEQ_1:3;
then A121: i in dom ((lower_volume (f,D1)) | k) by A117, FINSEQ_1:def 3;
then A122: i in dom ((lower_volume (f,D1)) | (Seg k)) by FINSEQ_1:def 15;
k <= k + 1 by NAT_1:11;
then A123: Seg k c= Seg (k + 1) by FINSEQ_1:7;
A124: dom ((lower_volume (f,D1)) | (k + 1)) = Seg (len ((lower_volume (f,D1)) | (k + 1))) by FINSEQ_1:def 3
.= Seg (k + 1) by A109, FINSEQ_1:80 ;
dom ((lower_volume (f,D1)) | k) = Seg (len ((lower_volume (f,D1)) | k)) by FINSEQ_1:def 3
.= Seg k by A116, FINSEQ_1:80 ;
then i in dom ((lower_volume (f,D1)) | (k + 1)) by A121, A123, A124;
then A125: i in dom ((lower_volume (f,D1)) | (Seg (k + 1))) by FINSEQ_1:def 15;
A126: ((lower_volume (f,D1)) | (k + 1)) . i = ((lower_volume (f,D1)) | (Seg (k + 1))) . i by FINSEQ_1:def 15
.= (lower_volume (f,D1)) . i by A125, FUNCT_1:70 ;
A127: ((lower_volume (f,D1)) | k) . i = ((lower_volume (f,D1)) | (Seg k)) . i by FINSEQ_1:def 15
.= (lower_volume (f,D1)) . i by A122, FUNCT_1:70 ;
i in dom p1 by A120, FINSEQ_1:def 3;
hence p1 . i = ((lower_volume (f,D1)) | k) . i by A113, A127, A126, FINSEQ_1:def 7; :: thesis: verum
end;
then A128: p1 = (lower_volume (f,D1)) | k by A117, FINSEQ_1:18;
A129: indx (D2,D1,(k + 1)) in dom D2 by A1, A104, Def21;
then A130: indx (D2,D1,(k + 1)) in Seg (len D2) by FINSEQ_1:def 3;
then A131: 1 <= indx (D2,D1,(k + 1)) by FINSEQ_1:3;
not k + 1 is trivial by A108, NAT_2:def 1;
then k + 1 >= 2 by NAT_2:31;
then k >= (1 + 1) - 1 by XREAL_1:22;
then A132: k in Seg (len D1) by A115, FINSEQ_1:3;
then A133: k in dom D1 by FINSEQ_1:def 3;
then A134: indx (D2,D1,k) in dom D2 by A1, Def21;
A135: indx (D2,D1,k) < indx (D2,D1,(k + 1))
proof
k < k + 1 by NAT_1:13;
then A136: D1 . k < D1 . (k + 1) by A104, A133, SEQM_3:def 1;
assume indx (D2,D1,k) >= indx (D2,D1,(k + 1)) ; :: thesis: contradiction
then A137: D2 . (indx (D2,D1,k)) >= D2 . (indx (D2,D1,(k + 1))) by A134, A129, SEQ_4:154;
D1 . k = D2 . (indx (D2,D1,k)) by A1, A133, Def21;
hence contradiction by A1, A104, A137, A136, Def21; :: thesis: verum
end;
A138: indx (D2,D1,(k + 1)) >= indx (D2,D1,k)
proof
assume indx (D2,D1,(k + 1)) < indx (D2,D1,k) ; :: thesis: contradiction
then A139: D2 . (indx (D2,D1,(k + 1))) < D2 . (indx (D2,D1,k)) by A134, A129, SEQM_3:def 1;
D1 . (k + 1) = D2 . (indx (D2,D1,(k + 1))) by A1, A104, Def21;
then D1 . (k + 1) < D1 . k by A1, A133, A139, Def21;
hence contradiction by A104, A133, NAT_1:11, SEQ_4:154; :: thesis: verum
end;
then consider ID being Nat such that
A140: indx (D2,D1,(k + 1)) = (indx (D2,D1,k)) + ID by NAT_1:10;
reconsider ID = ID as Element of NAT by ORDINAL1:def 13;
A141: len (lower_volume (f,D2)) = len D2 by Def8;
then A142: indx (D2,D1,(k + 1)) <= len (lower_volume (f,D2)) by A130, FINSEQ_1:3;
then len ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = (indx (D2,D1,k)) + ((indx (D2,D1,(k + 1))) - (indx (D2,D1,k))) by FINSEQ_1:80;
then consider p2, q2 being FinSequence of REAL such that
A143: len p2 = indx (D2,D1,k) and
A144: len q2 = (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) and
A145: (lower_volume (f,D2)) | (indx (D2,D1,(k + 1))) = p2 ^ q2 by A140, FINSEQ_2:26;
A146: indx (D2,D1,(k + 1)) <= len D2 by A130, FINSEQ_1:3;
indx (D2,D1,k) in dom D2 by A1, A133, Def21;
then A147: indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;
then A148: 1 <= indx (D2,D1,k) by FINSEQ_1:3;
A149: Sum q1 <= Sum q2
proof
set MD2 = mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))));
set MD1 = mid (D1,(k + 1),(k + 1));
set DD1 = divset (D1,(k + 1));
set g = f | (divset (D1,(k + 1)));
A150: 1 <= (indx (D2,D1,k)) + 1 by NAT_1:11;
reconsider g = f | (divset (D1,(k + 1))) as PartFunc of (divset (D1,(k + 1))),REAL by PARTFUN1:43;
(k + 1) - 1 = k ;
then A151: lower_bound (divset (D1,(k + 1))) = D1 . k by A104, A108, Def5;
dom g = (dom f) /\ (divset (D1,(k + 1))) by RELAT_1:90;
then dom g = A /\ (divset (D1,(k + 1))) by FUNCT_2:def 1;
then dom g = divset (D1,(k + 1)) by A104, Th10, XBOOLE_1:28;
then A152: g is total by PARTFUN1:def 4;
A153: upper_bound (divset (D1,(k + 1))) = D1 . (k + 1) by A104, A108, Def5;
A154: D2 . (indx (D2,D1,(k + 1))) = D1 . (k + 1) by A1, A104, Def21;
A155: (indx (D2,D1,k)) + 1 <= indx (D2,D1,(k + 1)) by A135, NAT_1:13;
then A156: (indx (D2,D1,k)) + 1 <= len D2 by A146, XXREAL_0:2;
then (indx (D2,D1,k)) + 1 in Seg (len D2) by A150, FINSEQ_1:3;
then A157: (indx (D2,D1,k)) + 1 in dom D2 by FINSEQ_1:def 3;
then D2 . ((indx (D2,D1,k)) + 1) >= D2 . (indx (D2,D1,k)) by A134, NAT_1:11, SEQ_4:154;
then D2 . ((indx (D2,D1,k)) + 1) >= lower_bound (divset (D1,(k + 1))) by A1, A133, A151, Def21;
then reconsider MD2 = mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))) as Division of divset (D1,(k + 1)) by A129, A155, A157, A154, A153, Th39;
A158: ((indx (D2,D1,(k + 1))) -' ((indx (D2,D1,k)) + 1)) + 1 = ((indx (D2,D1,(k + 1))) - ((indx (D2,D1,k)) + 1)) + 1 by A155, XREAL_1:235
.= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) ;
A159: for n being Nat st 1 <= n & n <= len q2 holds
q2 . n = (lower_volume (g,MD2)) . n
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len q2 implies q2 . n = (lower_volume (g,MD2)) . n )
assume that
A160: 1 <= n and
A161: n <= len q2 ; :: thesis: q2 . n = (lower_volume (g,MD2)) . n
A162: n in Seg (len q2) by A160, A161, FINSEQ_1:3;
then A163: n in dom q2 by FINSEQ_1:def 3;
then A164: (indx (D2,D1,k)) + n in dom ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A143, A145, FINSEQ_1:41;
then A165: (indx (D2,D1,k)) + n in dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 15;
A166: len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) = ID by A131, A146, A140, A155, A156, A150, A158, FINSEQ_6:124;
A167: dom ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = Seg (len ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 3
.= Seg (indx (D2,D1,(k + 1))) by A142, FINSEQ_1:80 ;
then (indx (D2,D1,k)) + n <= indx (D2,D1,(k + 1)) by A164, FINSEQ_1:3;
then A168: n <= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) by XREAL_1:21;
then n in Seg (len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))))) by A140, A160, A166, FINSEQ_1:3;
then A169: n in dom MD2 by FINSEQ_1:def 3;
A170: Seg (indx (D2,D1,(k + 1))) c= Seg (len D2) by A146, FINSEQ_1:7;
then (indx (D2,D1,k)) + n in Seg (len D2) by A167, A164;
then A171: (indx (D2,D1,k)) + n in dom D2 by FINSEQ_1:def 3;
A172: q2 . n = ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . ((indx (D2,D1,k)) + n) by A143, A145, A163, FINSEQ_1:def 7
.= ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . ((indx (D2,D1,k)) + n) by FINSEQ_1:def 15
.= (lower_volume (f,D2)) . ((indx (D2,D1,k)) + n) by A165, FUNCT_1:70
.= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,k)) + n)))))) * (vol (divset (D2,((indx (D2,D1,k)) + n)))) by A171, Def8 ;
A173: 1 <= (indx (D2,D1,k)) + n by A167, A164, FINSEQ_1:3;
A174: ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
proof
now
per cases ( n = 1 or n <> 1 ) ;
suppose A175: n = 1 ; :: thesis: ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
then A176: 1 <= (indx (D2,D1,k)) + 1 by A167, A164, FINSEQ_1:3;
A177: (indx (D2,D1,k)) + 1 <= len D2 by A167, A164, A170, A175, FINSEQ_1:3;
A178: upper_bound (divset (MD2,1)) = (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) . 1 by A169, A175, Def5
.= D2 . (1 + (indx (D2,D1,k))) by A131, A146, A176, A177, FINSEQ_6:124 ;
A179: (indx (D2,D1,k)) + 1 <> 1 by A148, NAT_1:13;
A180: (k + 1) - 1 = k ;
A181: lower_bound (divset (MD2,1)) = lower_bound (divset (D1,(k + 1))) by A169, A175, Def5
.= D1 . k by A104, A108, A180, Def5 ;
A182: divset (D2,((indx (D2,D1,k)) + n)) = [.(lower_bound (divset (D2,((indx (D2,D1,k)) + 1)))),(upper_bound (divset (D2,((indx (D2,D1,k)) + 1)))).] by A175, Th5
.= [.(D2 . (((indx (D2,D1,k)) + 1) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + 1)))).] by A157, A179, Def5
.= [.(D2 . (indx (D2,D1,k))),(D2 . ((indx (D2,D1,k)) + 1)).] by A157, A179, Def5
.= [.(D1 . k),(D2 . ((indx (D2,D1,k)) + 1)).] by A1, A133, Def21 ;
hence divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) by A175, A181, A178, Th5; :: thesis: ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
divset (MD2,n) = [.(D1 . k),(D2 . ((indx (D2,D1,k)) + 1)).] by A175, A181, A178, Th5;
hence ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) ) by A169, A182, Th10; :: thesis: verum
end;
suppose A183: n <> 1 ; :: thesis: ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
A184: (indx (D2,D1,k)) + n <> 1
proof
assume (indx (D2,D1,k)) + n = 1 ; :: thesis: contradiction
then indx (D2,D1,k) = 1 - n ;
then n + 1 <= 1 by A148, XREAL_1:21;
then n <= 1 - 1 by XREAL_1:21;
hence contradiction by A160, NAT_1:3; :: thesis: verum
end;
A185: divset (D2,((indx (D2,D1,k)) + n)) = [.(lower_bound (divset (D2,((indx (D2,D1,k)) + n)))),(upper_bound (divset (D2,((indx (D2,D1,k)) + n)))).] by Th5
.= [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + n)))).] by A171, A184, Def5
.= [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(D2 . ((indx (D2,D1,k)) + n)).] by A171, A184, Def5 ;
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:22;
then A186: n - 1 <= len MD2 by A140, A168, A166, XXREAL_0:2;
A187: (indx (D2,D1,k)) + 1 <= indx (D2,D1,(k + 1)) by A135, NAT_1:13;
not n is trivial by A160, A183, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:31;
then A188: 1 <= n - 1 by XREAL_1:21;
consider n1 being Nat such that
A189: n = 1 + n1 by A160, NAT_1:10;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 13;
A190: (n1 + ((indx (D2,D1,k)) + 1)) -' 1 = ((indx (D2,D1,k)) + n) - 1 by A173, A189, XREAL_1:235;
A191: (n + ((indx (D2,D1,k)) + 1)) -' 1 = ((n + (indx (D2,D1,k))) + 1) - 1 by NAT_1:11, XREAL_1:235
.= (indx (D2,D1,k)) + n ;
A192: lower_bound (divset (MD2,n)) = MD2 . (n - 1) by A169, A183, Def5
.= D2 . (((indx (D2,D1,k)) + n) - 1) by A131, A146, A156, A150, A187, A189, A190, A188, A186, FINSEQ_6:124 ;
A193: upper_bound (divset (MD2,n)) = MD2 . n by A169, A183, Def5
.= D2 . ((indx (D2,D1,k)) + n) by A131, A146, A140, A156, A150, A160, A162, A168, A166, A187, A191, FINSEQ_6:124 ;
hence divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) by A192, A185, Th5; :: thesis: ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
divset (MD2,n) = [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(D2 . ((indx (D2,D1,k)) + n)).] by A192, A193, Th5;
hence ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) ) by A169, A185, Th10; :: thesis: verum
end;
end;
end;
hence ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) ) ; :: thesis: verum
end;
then g | (divset (MD2,n)) = f | (divset (D2,((indx (D2,D1,k)) + n))) by FUNCT_1:82;
hence q2 . n = (lower_volume (g,MD2)) . n by A169, A172, A174, Def8; :: thesis: verum
end;
(k + 1) - 1 = k ;
then A194: lower_bound (divset (D1,(k + 1))) = D1 . k by A104, A108, Def5;
D1 . (k + 1) = upper_bound (divset (D1,(k + 1))) by A104, A108, Def5;
then reconsider MD1 = mid (D1,(k + 1),(k + 1)) as Division of divset (D1,(k + 1)) by A104, A114, A133, A194, Th39, SEQ_4:154;
A195: g | (divset (D1,(k + 1))) is bounded_below
proof
consider a being real number such that
A196: for x being set st x in A /\ (dom f) holds
a <= f . x by A2, RFUNCT_1:88;
for x being set st x in (divset (D1,(k + 1))) /\ (dom g) holds
a <= g . x
proof
let x be set ; :: thesis: ( x in (divset (D1,(k + 1))) /\ (dom g) implies a <= g . x )
A197: dom g c= dom f by RELAT_1:89;
assume x in (divset (D1,(k + 1))) /\ (dom g) ; :: thesis: a <= g . x
then A198: x in dom g by XBOOLE_0:def 4;
A199: A /\ (dom f) = dom f by XBOOLE_1:28;
then reconsider x = x as Element of A by A198, A197, XBOOLE_0:def 4;
a <= f . x by A196, A198, A199, A197;
hence a <= g . x by A198, FUNCT_1:70; :: thesis: verum
end;
hence g | (divset (D1,(k + 1))) is bounded_below by RFUNCT_1:88; :: thesis: verum
end;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A106, A107, FINSEQ_6:124;
then A200: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
A201: for n being Nat st 1 <= n & n <= len q1 holds
q1 . n = (lower_volume (g,MD1)) . n
proof
k + 1 in Seg (len ((lower_volume (f,D1)) | (k + 1))) by A110, FINSEQ_1:6;
then k + 1 in dom ((lower_volume (f,D1)) | (k + 1)) by FINSEQ_1:def 3;
then A202: k + 1 in dom ((lower_volume (f,D1)) | (Seg (k + 1))) by FINSEQ_1:def 15;
A203: ((lower_volume (f,D1)) | (k + 1)) . (k + 1) = ((lower_volume (f,D1)) | (Seg (k + 1))) . (k + 1) by FINSEQ_1:def 15
.= (lower_volume (f,D1)) . (k + 1) by A202, FUNCT_1:70 ;
A204: MD1 . 1 = D1 . (k + 1) by A106, A107, FINSEQ_6:124;
1 in Seg 1 by FINSEQ_1:5;
then A205: 1 in dom MD1 by A200, FINSEQ_1:def 3;
then A206: upper_bound (divset (MD1,1)) = MD1 . 1 by Def5;
let n be Nat; :: thesis: ( 1 <= n & n <= len q1 implies q1 . n = (lower_volume (g,MD1)) . n )
assume that
A207: 1 <= n and
A208: n <= len q1 ; :: thesis: q1 . n = (lower_volume (g,MD1)) . n
A209: n = 1 by A112, A207, A208, XXREAL_0:1;
lower_bound (divset (MD1,1)) = lower_bound (divset (D1,(k + 1))) by A205, Def5;
then A210: divset (MD1,1) = [.(lower_bound (divset (D1,(k + 1)))),(D1 . (k + 1)).] by A206, A204, Th5;
(k + 1) - 1 = k ;
then A211: lower_bound (divset (D1,(k + 1))) = D1 . k by A104, A108, Def5;
upper_bound (divset (D1,(k + 1))) = D1 . (k + 1) by A104, A108, Def5;
then A212: divset (D1,(k + 1)) = [.(D1 . k),(D1 . (k + 1)).] by A211, Th5;
A213: n in Seg (len q1) by A207, A208, FINSEQ_1:3;
then n in dom MD1 by A112, A200, FINSEQ_1:def 3;
then A214: (lower_volume (g,MD1)) . n = (lower_bound (rng (g | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1)))) by A209, A210, A211, A212, Def8;
n in dom q1 by A213, FINSEQ_1:def 3;
then q1 . n = (lower_volume (f,D1)) . (k + 1) by A111, A113, A209, A203, FINSEQ_1:def 7
.= (lower_bound (rng (f | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1)))) by A104, Def8 ;
hence q1 . n = (lower_volume (g,MD1)) . n by A214, FUNCT_1:82; :: thesis: verum
end;
len q1 = len (lower_volume (g,MD1)) by A112, A200, Def8;
then A215: q1 = lower_volume (g,MD1) by A201, FINSEQ_1:18;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A106, A107, FINSEQ_6:124;
then len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
then A216: lower_sum (g,MD1) <= lower_sum (g,MD2) by A195, A152, Th33;
len (lower_volume (g,MD2)) = len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) by Def8
.= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) by A131, A146, A155, A156, A150, A158, FINSEQ_6:124 ;
hence Sum q1 <= Sum q2 by A144, A215, A159, A216, FINSEQ_1:18; :: thesis: verum
end;
set KD2 = (lower_volume (f,D2)) | (indx (D2,D1,k));
A217: Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = (Sum p2) + (Sum q2) by A145, RVSUM_1:105;
A218: indx (D2,D1,k) <= len (lower_volume (f,D2)) by A141, A147, FINSEQ_1:3;
then A219: len p2 = len ((lower_volume (f,D2)) | (indx (D2,D1,k))) by A143, FINSEQ_1:80;
for i being Nat st 1 <= i & i <= len p2 holds
p2 . i = ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len p2 implies p2 . i = ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i )
assume that
A220: 1 <= i and
A221: i <= len p2 ; :: thesis: p2 . i = ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i
A222: i in Seg (len p2) by A220, A221, FINSEQ_1:3;
then A223: i in dom ((lower_volume (f,D2)) | (indx (D2,D1,k))) by A219, FINSEQ_1:def 3;
then A224: i in dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,k)))) by FINSEQ_1:def 15;
A225: dom ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = Seg (len ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 3
.= Seg (indx (D2,D1,(k + 1))) by A142, FINSEQ_1:80 ;
A226: Seg (indx (D2,D1,k)) c= Seg (indx (D2,D1,(k + 1))) by A138, FINSEQ_1:7;
dom ((lower_volume (f,D2)) | (indx (D2,D1,k))) = Seg (len ((lower_volume (f,D2)) | (indx (D2,D1,k)))) by FINSEQ_1:def 3
.= Seg (indx (D2,D1,k)) by A218, FINSEQ_1:80 ;
then i in dom ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A223, A226, A225;
then A227: i in dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 15;
A228: ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . i = ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . i by FINSEQ_1:def 15
.= (lower_volume (f,D2)) . i by A227, FUNCT_1:70 ;
A229: ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i = ((lower_volume (f,D2)) | (Seg (indx (D2,D1,k)))) . i by FINSEQ_1:def 15
.= (lower_volume (f,D2)) . i by A224, FUNCT_1:70 ;
i in dom p2 by A222, FINSEQ_1:def 3;
hence p2 . i = ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i by A145, A229, A228, FINSEQ_1:def 7; :: thesis: verum
end;
then A230: p2 = (lower_volume (f,D2)) | (indx (D2,D1,k)) by A219, FINSEQ_1:18;
Sum ((lower_volume (f,D1)) | (k + 1)) = (Sum p1) + (Sum q1) by A113, RVSUM_1:105;
then Sum q1 = (Sum ((lower_volume (f,D1)) | (k + 1))) - (Sum p1) ;
then Sum ((lower_volume (f,D1)) | (k + 1)) <= (Sum q2) + (Sum p1) by A149, XREAL_1:22;
then (Sum ((lower_volume (f,D1)) | (k + 1))) - (Sum q2) <= Sum p1 by XREAL_1:22;
then (Sum ((lower_volume (f,D1)) | (k + 1))) - (Sum q2) <= Sum p2 by A103, A132, A128, A230, FINSEQ_1:def 3, XXREAL_0:2;
hence Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A217, XREAL_1:22; :: thesis: verum
end;
end;
end;
hence Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) ; :: thesis: verum
end;
thus for n being non empty Nat holds S1[n] from NAT_1:sch 10(A3, A102); :: thesis: verum
end;
hence for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume (f,D1)) | i) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i))) ; :: thesis: verum