let A be non empty 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 zero 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 zero 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 zero 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 zero 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 zero 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:10;
A4: dom g = (dom f) /\ (divset (D1,1)) by RELAT_1:61;
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 Def3;
then A7: D2 . (indx (D2,D1,1)) = upper_bound (divset (D1,1)) by A1, A5, Def18;
lower_bound (divset (D1,1)) <= upper_bound (divset (D1,1)) by SEQ_4:11;
then reconsider DD1 = mid (D1,1,1) as Division of divset (D1,1) by A5, A6, Th35;
1 in Seg (len D1) by A5, FINSEQ_1:def 3;
then A8: 1 <= len D1 by FINSEQ_1:1;
then A9: len (mid (D1,1,1)) = (1 -' 1) + 1 by FINSEQ_6:118;
A10: len (lower_volume (g,DD1)) = len DD1 by Def6
.= 1 by A9, XREAL_1:235 ;
A11: len (mid (D1,1,1)) = 1 by A9, XREAL_1:235;
then A12: len (mid (D1,1,1)) = len (D1 | 1) ;
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:1;
then k in dom (D1 | 1) by FINSEQ_1:def 3;
then k in dom (D1 | (Seg 1)) by FINSEQ_1:def 16;
then A15: (D1 | (Seg 1)) . k = D1 . k by FUNCT_1:47;
A16: k = 1 by A11, A13, A14, XXREAL_0:1;
then (mid (D1,1,1)) . k = D1 . ((1 + 1) - 1) by A8, FINSEQ_6:118;
hence (mid (D1,1,1)) . k = (D1 | 1) . k by A16, A15, FINSEQ_1:def 16; :: thesis: verum
end;
then A17: mid (D1,1,1) = D1 | 1 by A12, FINSEQ_1:14;
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:3;
dom (D1 | (Seg 1)) = (dom D1) /\ (Seg 1) by RELAT_1:61;
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 Def6 ;
then A23: dom ((lower_volume (f,D1)) | (Seg 1)) = (Seg (len D1)) /\ (Seg 1) by RELAT_1:61
.= Seg 1 by A8, FINSEQ_1:7 ;
len DD1 = 1 by A9, XREAL_1:235;
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 16
.= ((lower_volume (f,D1)) | (Seg 1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (lower_volume (f,D1)) . 1 by A23, FINSEQ_1:3, FUNCT_1:47
.= (lower_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) by A5, Def6 ;
A26: divset (D1,1) = [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by Th2
.= [.(lower_bound A),(upper_bound (divset (D1,1))).] by A5, Def3
.= [.(lower_bound A),(D1 . 1).] by A5, Def3 ;
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, Def6 ;
divset (DD1,1) = [.(lower_bound (divset (DD1,1))),(upper_bound (divset (DD1,1))).] by Th2
.= [.(lower_bound (divset (D1,1))),(upper_bound (divset (DD1,1))).] by A24, Def3
.= [.(lower_bound (divset (D1,1))),(DD1 . 1).] by A24, Def3
.= [.(lower_bound A),((D1 | 1) . 1).] by A5, A17, Def3
.= [.(lower_bound A),((D1 | (Seg 1)) . 1).] by FINSEQ_1:def 16
.= [.(lower_bound A),(D1 . 1).] by A22, FUNCT_1:47 ;
hence (lower_volume (g,DD1)) . i = ((lower_volume (f,D1)) | 1) . i by A27, A26, A25; :: thesis: verum
end;
A28: g | (divset (D1,1)) is bounded_below
proof
consider a being Real such that
A29: for x being object st x in A /\ (dom f) holds
a <= f . x by A2, RFUNCT_1:71;
for x being object st x in (divset (D1,1)) /\ (dom g) holds
a <= g . x
proof
let x be object ; :: thesis: ( x in (divset (D1,1)) /\ (dom g) implies a <= g . x )
A30: dom g c= dom f by RELAT_1:60;
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:47; :: thesis: verum
end;
hence g | (divset (D1,1)) is bounded_below by RFUNCT_1:71; :: thesis: verum
end;
A33: rng D2 c= A by Def1;
A34: indx (D2,D1,1) in dom D2 by A1, A5, Def18;
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:1;
A37: indx (D2,D1,1) <= len D2 by A35, FINSEQ_1:1;
then 1 <= len D2 by A36, XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:1;
then A38: 1 in dom D2 by FINSEQ_1:def 3;
then D2 . 1 in rng D2 by FUNCT_1:def 3;
then D2 . 1 in A by A33;
then D2 . 1 in [.(lower_bound A),(upper_bound A).] by Th2;
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, Def3;
then reconsider DD2 = mid (D2,1,(indx (D2,D1,1))) as Division of divset (D1,1) by A34, A36, A38, A7, Th35;
indx (D2,D1,1) in dom D2 by A1, A5, Def18;
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:1;
A41: indx (D2,D1,1) <= len D2 by A39, FINSEQ_1:1;
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:118;
then A43: len (mid (D2,1,(indx (D2,D1,1)))) = ((indx (D2,D1,1)) - 1) + 1 by A40, XREAL_1:233;
then A44: len (mid (D2,1,(indx (D2,D1,1)))) = len (D2 | (indx (D2,D1,1))) by A41, FINSEQ_1:59;
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
k in Seg (len (D2 | (indx (D2,D1,1)))) by A44, A46, A47, FINSEQ_1:1;
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 16;
then A48: (D2 | (Seg (indx (D2,D1,1)))) . k = D2 . k by FUNCT_1:47;
(mid (D2,1,(indx (D2,D1,1)))) . k = D2 . ((k + 1) -' 1) by A40, A41, A42, A46, A47, FINSEQ_6:118;
then (mid (D2,1,(indx (D2,D1,1)))) . k = D2 . ((k + 1) - 1) by NAT_1:11, XREAL_1:233;
hence (mid (D2,1,(indx (D2,D1,1)))) . k = (D2 | (indx (D2,D1,1))) . k by A48, FINSEQ_1:def 16; :: thesis: verum
end;
then A49: mid (D2,1,(indx (D2,D1,1))) = D2 | (indx (D2,D1,1)) by A44, FINSEQ_1:14;
A50: 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
A51: 1 <= i and
A52: i <= len (lower_volume (g,DD2)) ; :: thesis: (lower_volume (g,DD2)) . i = ((lower_volume (f,D2)) | (indx (D2,D1,1))) . i
A53: i <= len DD2 by A52, Def6;
then A54: i in Seg (len DD2) by A51, FINSEQ_1:1;
then A55: 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:5;
then i in Seg (len D2) by A43, A54;
then A56: i in dom D2 by FINSEQ_1:def 3;
now :: thesis: divset (DD2,i) = divset (D2,i)
per cases ( i = 1 or i <> 1 ) ;
suppose A57: i = 1 ; :: thesis: divset (DD2,i) = divset (D2,i)
then A58: 1 in dom (D2 | (Seg (indx (D2,D1,1)))) by A49, A55, FINSEQ_1:def 16;
then 1 in (dom D2) /\ (Seg (indx (D2,D1,1))) by RELAT_1:61;
then A59: 1 in dom D2 by XBOOLE_0:def 4;
A60: divset (D2,i) = [.(lower_bound (divset (D2,1))),(upper_bound (divset (D2,1))).] by A57, Th2
.= [.(lower_bound A),(upper_bound (divset (D2,1))).] by A59, Def3
.= [.(lower_bound A),(D2 . 1).] by A59, Def3 ;
divset (DD2,i) = [.(lower_bound (divset (DD2,1))),(upper_bound (divset (DD2,1))).] by A57, Th2
.= [.(lower_bound (divset (D1,1))),(upper_bound (divset (DD2,1))).] by A55, A57, Def3
.= [.(lower_bound (divset (D1,1))),(DD2 . 1).] by A55, A57, Def3
.= [.(lower_bound (divset (D1,1))),((D2 | (indx (D2,D1,1))) . 1).] by A45, A53, A57
.= [.(lower_bound (divset (D1,1))),((D2 | (Seg (indx (D2,D1,1)))) . 1).] by FINSEQ_1:def 16
.= [.(lower_bound (divset (D1,1))),(D2 . 1).] by A58, FUNCT_1:47
.= [.(lower_bound A),(D2 . 1).] by A5, Def3 ;
hence divset (DD2,i) = divset (D2,i) by A60; :: thesis: verum
end;
suppose A61: i <> 1 ; :: thesis: divset (DD2,i) = divset (D2,i)
A62: 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:14
.= (D2 | (Seg (indx (D2,D1,1)))) . (i - 1) by FINSEQ_1:def 16 ;
then A68: DD2 . (i - 1) = D2 . (i - 1) by A62, FUNCT_1:47;
i <= len D2 by A43, A37, A53, XXREAL_0:2;
then i in Seg (len D2) by A51, FINSEQ_1:1;
then i in dom D2 by FINSEQ_1:def 3;
then i in (dom D2) /\ (Seg (indx (D2,D1,1))) by A43, A54, XBOOLE_0:def 4;
then A69: i in dom (D2 | (Seg (indx (D2,D1,1)))) by RELAT_1:61;
DD2 . i = (D2 | (indx (D2,D1,1))) . i by A44, A45, FINSEQ_1:14
.= (D2 | (Seg (indx (D2,D1,1)))) . i by FINSEQ_1:def 16 ;
then A70: DD2 . i = D2 . i by A69, FUNCT_1:47;
A71: divset (D2,i) = [.(lower_bound (divset (D2,i))),(upper_bound (divset (D2,i))).] by Th2
.= [.(D2 . (i - 1)),(upper_bound (divset (D2,i))).] by A56, A61, Def3
.= [.(D2 . (i - 1)),(D2 . i).] by A56, A61, Def3 ;
divset (DD2,i) = [.(lower_bound (divset (DD2,i))),(upper_bound (divset (DD2,i))).] by Th2
.= [.(DD2 . (i - 1)),(upper_bound (divset (DD2,i))).] by A55, A61, Def3
.= [.(D2 . (i - 1)),(D2 . i).] by A55, A61, A68, A70, Def3 ;
hence divset (DD2,i) = divset (D2,i) by A71; :: thesis: verum
end;
end;
end;
hence divset (DD2,i) = divset (D2,i) ; :: thesis: verum
end;
then A72: (lower_volume (g,DD2)) . i = (lower_bound (rng (g | (divset (D2,i))))) * (vol (divset (D2,i))) by A55, Def6;
Seg (indx (D2,D1,1)) c= Seg (len D2) by A41, FINSEQ_1:5;
then i in Seg (len D2) by A43, A54;
then A73: i in dom D2 by FINSEQ_1:def 3;
A74: i in dom DD2 by A54, FINSEQ_1:def 3;
A75: now :: 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))).] )
per cases ( i = 1 or i <> 1 ) ;
suppose A76: 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 A49, A74, FINSEQ_1:def 16;
then 1 in (dom D2) /\ (Seg (indx (D2,D1,1))) by RELAT_1:61;
then A77: 1 in dom D2 by XBOOLE_0:def 4;
then D2 . 1 <= D2 . (indx (D2,D1,1)) by A34, A36, SEQ_4:137;
then A78: D2 . 1 <= D1 . 1 by A1, A5, Def18;
lower_bound (divset (D2,i)) = lower_bound A by A76, A77, Def3;
then A79: lower_bound (divset (D2,i)) = lower_bound (divset (D1,1)) by A5, Def3;
upper_bound (divset (D2,i)) = D2 . 1 by A76, A77, Def3;
then A80: upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A5, A78, Def3;
lower_bound (divset (D1,1)) <= upper_bound (divset (D1,1)) by SEQ_4:11;
hence lower_bound (divset (D2,i)) in [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by A79, 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 SEQ_4:11;
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 A79, A80;
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 A81: 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 A51, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:29;
then A82: 1 <= i - 1 by XREAL_1:19;
A83: ex j being Nat st i = 1 + j by A51, NAT_1:10;
A84: rng D2 c= A by Def1;
A85: lower_bound (divset (D2,i)) = D2 . (i - 1) by A73, A81, Def3;
A86: lower_bound (divset (D1,1)) = lower_bound A by A5, Def3;
A87: i - 1 <= (indx (D2,D1,1)) - 0 by A43, A53, XREAL_1:13;
then i - 1 <= len D2 by A37, XXREAL_0:2;
then i - 1 in Seg (len D2) by A83, A82, FINSEQ_1:1;
then A88: i - 1 in dom D2 by FINSEQ_1:def 3;
then D2 . (i - 1) in rng D2 by FUNCT_1:def 3;
then A89: lower_bound (divset (D2,i)) >= lower_bound (divset (D1,1)) by A85, A86, A84, SEQ_4:def 2;
A90: upper_bound (divset (D1,1)) = D1 . 1 by A5, Def3;
D2 . (i - 1) <= D2 . (indx (D2,D1,1)) by A34, A87, A88, SEQ_4:137;
then lower_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A1, A5, A85, A90, Def18;
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 A89;
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))).]
A91: upper_bound (divset (D2,i)) = D2 . i by A73, A81, Def3;
D2 . i in rng D2 by A73, FUNCT_1:def 3;
then A92: upper_bound (divset (D2,i)) >= lower_bound (divset (D1,1)) by A91, A86, A84, SEQ_4:def 2;
D2 . i <= D2 . (indx (D2,D1,1)) by A43, A34, A53, A73, SEQ_4:137;
then upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A1, A5, A91, A90, Def18;
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 A92;
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;
A93: divset (D1,1) = [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by Th2;
A94: Seg (indx (D2,D1,1)) c= Seg (len D2) by A41, FINSEQ_1:5;
then i in Seg (len D2) by A43, A54;
then A95: i in dom D2 by FINSEQ_1:def 3;
divset (D2,i) = [.(lower_bound (divset (D2,i))),(upper_bound (divset (D2,i))).] by Th2;
then A96: divset (D2,i) c= divset (D1,1) by A93, A75, XXREAL_2:def 12;
A97: dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,1)))) = (dom (lower_volume (f,D2))) /\ (Seg (indx (D2,D1,1))) by RELAT_1:61
.= (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 Def6
.= Seg (indx (D2,D1,1)) by A94, 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 16
.= (lower_volume (f,D2)) . i by A43, A54, A97, FUNCT_1:47
.= (lower_bound (rng (f | (divset (D2,i))))) * (vol (divset (D2,i))) by A95, Def6 ;
hence (lower_volume (g,DD2)) . i = ((lower_volume (f,D2)) | (indx (D2,D1,1))) . i by A72, A96, FUNCT_1:51; :: thesis: verum
end;
len (lower_volume (g,DD1)) = len ((lower_volume (f,D1)) | 1) by A10;
then A98: lower_volume (g,DD1) = (lower_volume (f,D1)) | 1 by A18, FINSEQ_1:14;
A99: indx (D2,D1,1) <= len (lower_volume (f,D2)) by A41, Def6;
len (lower_volume (g,DD2)) = indx (D2,D1,1) by A43, Def6;
then A100: len (lower_volume (g,DD2)) = len ((lower_volume (f,D2)) | (indx (D2,D1,1))) by A99, FINSEQ_1:59;
dom g = A /\ (divset (D1,1)) by A4, FUNCT_2:def 1;
then dom g = divset (D1,1) by A5, Th6, XBOOLE_1:28;
then g is total by PARTFUN1:def 2;
then lower_sum (g,DD1) <= lower_sum (g,DD2) by A11, A28, Th29;
hence Sum ((lower_volume (f,D1)) | 1) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,1))) by A98, A100, A50, FINSEQ_1:14; :: thesis: verum
end;
A101: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A102: ( 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 A103: k + 1 in dom D1 ; :: thesis: Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))
then A104: k + 1 in Seg (len D1) by FINSEQ_1:def 3;
then A105: 1 <= k + 1 by FINSEQ_1:1;
A106: k + 1 <= len D1 by A104, FINSEQ_1:1;
now :: thesis: Sum ((lower_volume (f,D1)) | (k + 1)) <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1))))
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, A103; :: thesis: verum
end;
suppose A107: 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;
A108: k + 1 <= len (lower_volume (f,D1)) by A106, Def6;
then A109: len ((lower_volume (f,D1)) | (k + 1)) = k + 1 by FINSEQ_1:59;
then consider p1, q1 being FinSequence of REAL such that
A110: len p1 = k and
A111: len q1 = 1 and
A112: (lower_volume (f,D1)) | (k + 1) = p1 ^ q1 by FINSEQ_2:23;
A113: k <= k + 1 by NAT_1:11;
then A114: k <= len D1 by A106, XXREAL_0:2;
then A115: k <= len (lower_volume (f,D1)) by Def6;
then A116: len p1 = len ((lower_volume (f,D1)) | k) by A110, FINSEQ_1:59;
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
A117: 1 <= i and
A118: i <= len p1 ; :: thesis: p1 . i = ((lower_volume (f,D1)) | k) . i
A119: i in Seg (len p1) by A117, A118, FINSEQ_1:1;
then A120: i in dom ((lower_volume (f,D1)) | k) by A116, FINSEQ_1:def 3;
then A121: i in dom ((lower_volume (f,D1)) | (Seg k)) by FINSEQ_1:def 16;
k <= k + 1 by NAT_1:11;
then A122: Seg k c= Seg (k + 1) by FINSEQ_1:5;
A123: dom ((lower_volume (f,D1)) | (k + 1)) = Seg (len ((lower_volume (f,D1)) | (k + 1))) by FINSEQ_1:def 3
.= Seg (k + 1) by A108, FINSEQ_1:59 ;
dom ((lower_volume (f,D1)) | k) = Seg (len ((lower_volume (f,D1)) | k)) by FINSEQ_1:def 3
.= Seg k by A115, FINSEQ_1:59 ;
then i in dom ((lower_volume (f,D1)) | (k + 1)) by A120, A122, A123;
then A124: i in dom ((lower_volume (f,D1)) | (Seg (k + 1))) by FINSEQ_1:def 16;
A125: ((lower_volume (f,D1)) | (k + 1)) . i = ((lower_volume (f,D1)) | (Seg (k + 1))) . i by FINSEQ_1:def 16
.= (lower_volume (f,D1)) . i by A124, FUNCT_1:47 ;
A126: ((lower_volume (f,D1)) | k) . i = ((lower_volume (f,D1)) | (Seg k)) . i by FINSEQ_1:def 16
.= (lower_volume (f,D1)) . i by A121, FUNCT_1:47 ;
i in dom p1 by A119, FINSEQ_1:def 3;
hence p1 . i = ((lower_volume (f,D1)) | k) . i by A112, A126, A125, FINSEQ_1:def 7; :: thesis: verum
end;
then A127: p1 = (lower_volume (f,D1)) | k by A116, FINSEQ_1:14;
A128: indx (D2,D1,(k + 1)) in dom D2 by A1, A103, Def18;
then A129: indx (D2,D1,(k + 1)) in Seg (len D2) by FINSEQ_1:def 3;
then A130: 1 <= indx (D2,D1,(k + 1)) by FINSEQ_1:1;
not k + 1 is trivial by A107, NAT_2:def 1;
then k + 1 >= 2 by NAT_2:29;
then k >= (1 + 1) - 1 by XREAL_1:20;
then A131: k in Seg (len D1) by A114, FINSEQ_1:1;
then A132: k in dom D1 by FINSEQ_1:def 3;
then A133: indx (D2,D1,k) in dom D2 by A1, Def18;
A134: indx (D2,D1,k) < indx (D2,D1,(k + 1))
proof
k < k + 1 by NAT_1:13;
then A135: D1 . k < D1 . (k + 1) by A103, A132, SEQM_3:def 1;
assume indx (D2,D1,k) >= indx (D2,D1,(k + 1)) ; :: thesis: contradiction
then A136: D2 . (indx (D2,D1,k)) >= D2 . (indx (D2,D1,(k + 1))) by A133, A128, SEQ_4:137;
D1 . k = D2 . (indx (D2,D1,k)) by A1, A132, Def18;
hence contradiction by A1, A103, A136, A135, Def18; :: thesis: verum
end;
A137: indx (D2,D1,(k + 1)) >= indx (D2,D1,k)
proof
assume indx (D2,D1,(k + 1)) < indx (D2,D1,k) ; :: thesis: contradiction
then A138: D2 . (indx (D2,D1,(k + 1))) < D2 . (indx (D2,D1,k)) by A133, A128, SEQM_3:def 1;
D1 . (k + 1) = D2 . (indx (D2,D1,(k + 1))) by A1, A103, Def18;
then D1 . (k + 1) < D1 . k by A1, A132, A138, Def18;
hence contradiction by A103, A132, NAT_1:11, SEQ_4:137; :: thesis: verum
end;
then consider ID being Nat such that
A139: indx (D2,D1,(k + 1)) = (indx (D2,D1,k)) + ID by NAT_1:10;
reconsider ID = ID as Element of NAT by ORDINAL1:def 12;
A140: len (lower_volume (f,D2)) = len D2 by Def6;
then A141: indx (D2,D1,(k + 1)) <= len (lower_volume (f,D2)) by A129, FINSEQ_1:1;
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:59;
then consider p2, q2 being FinSequence of REAL such that
A142: len p2 = indx (D2,D1,k) and
A143: len q2 = (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) and
A144: (lower_volume (f,D2)) | (indx (D2,D1,(k + 1))) = p2 ^ q2 by A139, FINSEQ_2:23;
A145: indx (D2,D1,(k + 1)) <= len D2 by A129, FINSEQ_1:1;
indx (D2,D1,k) in dom D2 by A1, A132, Def18;
then A146: indx (D2,D1,k) in Seg (len D2) by FINSEQ_1:def 3;
then A147: 1 <= indx (D2,D1,k) by FINSEQ_1:1;
A148: 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)));
A149: 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:10;
(k + 1) - 1 = k ;
then A150: lower_bound (divset (D1,(k + 1))) = D1 . k by A103, A107, Def3;
dom g = (dom f) /\ (divset (D1,(k + 1))) by RELAT_1:61;
then dom g = A /\ (divset (D1,(k + 1))) by FUNCT_2:def 1;
then dom g = divset (D1,(k + 1)) by A103, Th6, XBOOLE_1:28;
then A151: g is total by PARTFUN1:def 2;
A152: upper_bound (divset (D1,(k + 1))) = D1 . (k + 1) by A103, A107, Def3;
A153: D2 . (indx (D2,D1,(k + 1))) = D1 . (k + 1) by A1, A103, Def18;
A154: (indx (D2,D1,k)) + 1 <= indx (D2,D1,(k + 1)) by A134, NAT_1:13;
then A155: (indx (D2,D1,k)) + 1 <= len D2 by A145, XXREAL_0:2;
then (indx (D2,D1,k)) + 1 in Seg (len D2) by A149, FINSEQ_1:1;
then A156: (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 A133, NAT_1:11, SEQ_4:137;
then D2 . ((indx (D2,D1,k)) + 1) >= lower_bound (divset (D1,(k + 1))) by A1, A132, A150, Def18;
then reconsider MD2 = mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))) as Division of divset (D1,(k + 1)) by A128, A154, A156, A153, A152, Th35;
A157: ((indx (D2,D1,(k + 1))) -' ((indx (D2,D1,k)) + 1)) + 1 = ((indx (D2,D1,(k + 1))) - ((indx (D2,D1,k)) + 1)) + 1 by A154, XREAL_1:233
.= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) ;
A158: 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
A159: 1 <= n and
A160: n <= len q2 ; :: thesis: q2 . n = (lower_volume (g,MD2)) . n
n in Seg (len q2) by A159, A160, FINSEQ_1:1;
then A161: n in dom q2 by FINSEQ_1:def 3;
then A162: (indx (D2,D1,k)) + n in dom ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A142, A144, FINSEQ_1:28;
then A163: (indx (D2,D1,k)) + n in dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 16;
A164: len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) = ID by A130, A145, A139, A154, A155, A149, A157, FINSEQ_6:118;
A165: 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 A141, FINSEQ_1:59 ;
then (indx (D2,D1,k)) + n <= indx (D2,D1,(k + 1)) by A162, FINSEQ_1:1;
then A166: n <= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) by XREAL_1:19;
then n in Seg (len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))))) by A139, A159, A164, FINSEQ_1:1;
then A167: n in dom MD2 by FINSEQ_1:def 3;
A168: Seg (indx (D2,D1,(k + 1))) c= Seg (len D2) by A145, FINSEQ_1:5;
then (indx (D2,D1,k)) + n in Seg (len D2) by A165, A162;
then A169: (indx (D2,D1,k)) + n in dom D2 by FINSEQ_1:def 3;
A170: q2 . n = ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . ((indx (D2,D1,k)) + n) by A142, A144, A161, FINSEQ_1:def 7
.= ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . ((indx (D2,D1,k)) + n) by FINSEQ_1:def 16
.= (lower_volume (f,D2)) . ((indx (D2,D1,k)) + n) by A163, FUNCT_1:47
.= (lower_bound (rng (f | (divset (D2,((indx (D2,D1,k)) + n)))))) * (vol (divset (D2,((indx (D2,D1,k)) + n)))) by A169, Def6 ;
A171: 1 <= (indx (D2,D1,k)) + n by A165, A162, FINSEQ_1:1;
A172: ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) )
proof
now :: 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)) )
per cases ( n = 1 or n <> 1 ) ;
suppose A173: 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 A174: 1 <= (indx (D2,D1,k)) + 1 by A165, A162, FINSEQ_1:1;
A175: (indx (D2,D1,k)) + 1 <= len D2 by A165, A162, A168, A173, FINSEQ_1:1;
A176: upper_bound (divset (MD2,1)) = (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) . 1 by A167, A173, Def3
.= D2 . (1 + (indx (D2,D1,k))) by A130, A145, A174, A175, FINSEQ_6:118 ;
A177: (indx (D2,D1,k)) + 1 <> 1 by A147, NAT_1:13;
A178: (k + 1) - 1 = k ;
A179: lower_bound (divset (MD2,1)) = lower_bound (divset (D1,(k + 1))) by A167, A173, Def3
.= D1 . k by A103, A107, A178, Def3 ;
A180: 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 A173, Th2
.= [.(D2 . (((indx (D2,D1,k)) + 1) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + 1)))).] by A156, A177, Def3
.= [.(D2 . (indx (D2,D1,k))),(D2 . ((indx (D2,D1,k)) + 1)).] by A156, A177, Def3
.= [.(D1 . k),(D2 . ((indx (D2,D1,k)) + 1)).] by A1, A132, Def18 ;
hence divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) by A173, A179, A176, Th2; :: 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 A173, A179, A176, Th2;
hence ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) ) by A167, A180, Th6; :: thesis: verum
end;
suppose A181: 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)) )
A182: (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 A147, XREAL_1:19;
then n <= 1 - 1 by XREAL_1:19;
hence contradiction by A159, NAT_1:3; :: thesis: verum
end;
A183: 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 Th2
.= [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + n)))).] by A169, A182, Def3
.= [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(D2 . ((indx (D2,D1,k)) + n)).] by A169, A182, Def3 ;
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:20;
then A184: n - 1 <= len MD2 by A139, A166, A164, XXREAL_0:2;
A185: (indx (D2,D1,k)) + 1 <= indx (D2,D1,(k + 1)) by A134, NAT_1:13;
not n is trivial by A159, A181, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:29;
then A186: 1 <= n - 1 by XREAL_1:19;
consider n1 being Nat such that
A187: n = 1 + n1 by A159, NAT_1:10;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 12;
A188: (n1 + ((indx (D2,D1,k)) + 1)) -' 1 = ((indx (D2,D1,k)) + n) - 1 by A171, A187, XREAL_1:233;
A189: (n + ((indx (D2,D1,k)) + 1)) -' 1 = ((n + (indx (D2,D1,k))) + 1) - 1 by NAT_1:11, XREAL_1:233
.= (indx (D2,D1,k)) + n ;
A190: lower_bound (divset (MD2,n)) = MD2 . (n - 1) by A167, A181, Def3
.= D2 . (((indx (D2,D1,k)) + n) - 1) by A130, A145, A155, A149, A185, A187, A188, A186, A184, FINSEQ_6:118 ;
A191: upper_bound (divset (MD2,n)) = MD2 . n by A167, A181, Def3
.= D2 . ((indx (D2,D1,k)) + n) by A130, A145, A139, A155, A149, A159, A166, A164, A185, A189, FINSEQ_6:118 ;
hence divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) by A190, A183, Th2; :: 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 A190, A191, Th2;
hence ( divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) & divset (D2,((indx (D2,D1,k)) + n)) c= divset (D1,(k + 1)) ) by A167, A183, Th6; :: 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:51;
hence q2 . n = (lower_volume (g,MD2)) . n by A167, A170, A172, Def6; :: thesis: verum
end;
(k + 1) - 1 = k ;
then A192: lower_bound (divset (D1,(k + 1))) = D1 . k by A103, A107, Def3;
D1 . (k + 1) = upper_bound (divset (D1,(k + 1))) by A103, A107, Def3;
then reconsider MD1 = mid (D1,(k + 1),(k + 1)) as Division of divset (D1,(k + 1)) by A103, A113, A132, A192, Th35, SEQ_4:137;
A193: g | (divset (D1,(k + 1))) is bounded_below
proof
consider a being Real such that
A194: for x being object st x in A /\ (dom f) holds
a <= f . x by A2, RFUNCT_1:71;
for x being object st x in (divset (D1,(k + 1))) /\ (dom g) holds
a <= g . x
proof
let x be object ; :: thesis: ( x in (divset (D1,(k + 1))) /\ (dom g) implies a <= g . x )
A195: dom g c= dom f by RELAT_1:60;
assume x in (divset (D1,(k + 1))) /\ (dom g) ; :: thesis: a <= g . x
then A196: x in dom g by XBOOLE_0:def 4;
A197: A /\ (dom f) = dom f by XBOOLE_1:28;
then reconsider x = x as Element of A by A196, A195, XBOOLE_0:def 4;
a <= f . x by A194, A196, A197, A195;
hence a <= g . x by A196, FUNCT_1:47; :: thesis: verum
end;
hence g | (divset (D1,(k + 1))) is bounded_below by RFUNCT_1:71; :: thesis: verum
end;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A105, A106, FINSEQ_6:118;
then A198: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:233;
A199: 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 A109, FINSEQ_1:4;
then k + 1 in dom ((lower_volume (f,D1)) | (k + 1)) by FINSEQ_1:def 3;
then A200: k + 1 in dom ((lower_volume (f,D1)) | (Seg (k + 1))) by FINSEQ_1:def 16;
A201: ((lower_volume (f,D1)) | (k + 1)) . (k + 1) = ((lower_volume (f,D1)) | (Seg (k + 1))) . (k + 1) by FINSEQ_1:def 16
.= (lower_volume (f,D1)) . (k + 1) by A200, FUNCT_1:47 ;
A202: MD1 . 1 = D1 . (k + 1) by A105, A106, FINSEQ_6:118;
1 in Seg 1 by FINSEQ_1:3;
then A203: 1 in dom MD1 by A198, FINSEQ_1:def 3;
then A204: upper_bound (divset (MD1,1)) = MD1 . 1 by Def3;
let n be Nat; :: thesis: ( 1 <= n & n <= len q1 implies q1 . n = (lower_volume (g,MD1)) . n )
assume that
A205: 1 <= n and
A206: n <= len q1 ; :: thesis: q1 . n = (lower_volume (g,MD1)) . n
A207: n = 1 by A111, A205, A206, XXREAL_0:1;
lower_bound (divset (MD1,1)) = lower_bound (divset (D1,(k + 1))) by A203, Def3;
then A208: divset (MD1,1) = [.(lower_bound (divset (D1,(k + 1)))),(D1 . (k + 1)).] by A204, A202, Th2;
(k + 1) - 1 = k ;
then A209: lower_bound (divset (D1,(k + 1))) = D1 . k by A103, A107, Def3;
upper_bound (divset (D1,(k + 1))) = D1 . (k + 1) by A103, A107, Def3;
then A210: divset (D1,(k + 1)) = [.(D1 . k),(D1 . (k + 1)).] by A209, Th2;
A211: n in Seg (len q1) by A205, A206, FINSEQ_1:1;
then n in dom MD1 by A111, A198, FINSEQ_1:def 3;
then A212: (lower_volume (g,MD1)) . n = (lower_bound (rng (g | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1)))) by A207, A208, A209, A210, Def6;
n in dom q1 by A211, FINSEQ_1:def 3;
then q1 . n = (lower_volume (f,D1)) . (k + 1) by A110, A112, A207, A201, FINSEQ_1:def 7
.= (lower_bound (rng (f | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1)))) by A103, Def6 ;
hence q1 . n = (lower_volume (g,MD1)) . n by A212; :: thesis: verum
end;
len q1 = len (lower_volume (g,MD1)) by A111, A198, Def6;
then A213: q1 = lower_volume (g,MD1) by A199, FINSEQ_1:14;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A105, A106, FINSEQ_6:118;
then len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:233;
then A214: lower_sum (g,MD1) <= lower_sum (g,MD2) by A193, A151, Th29;
len (lower_volume (g,MD2)) = len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) by Def6
.= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) by A130, A145, A154, A155, A149, A157, FINSEQ_6:118 ;
hence Sum q1 <= Sum q2 by A143, A213, A158, A214, FINSEQ_1:14; :: thesis: verum
end;
set KD2 = (lower_volume (f,D2)) | (indx (D2,D1,k));
A215: Sum ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = (Sum p2) + (Sum q2) by A144, RVSUM_1:75;
A216: indx (D2,D1,k) <= len (lower_volume (f,D2)) by A140, A146, FINSEQ_1:1;
then A217: len p2 = len ((lower_volume (f,D2)) | (indx (D2,D1,k))) by A142, FINSEQ_1:59;
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
A218: 1 <= i and
A219: i <= len p2 ; :: thesis: p2 . i = ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i
A220: i in Seg (len p2) by A218, A219, FINSEQ_1:1;
then A221: i in dom ((lower_volume (f,D2)) | (indx (D2,D1,k))) by A217, FINSEQ_1:def 3;
then A222: i in dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,k)))) by FINSEQ_1:def 16;
A223: 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 A141, FINSEQ_1:59 ;
A224: Seg (indx (D2,D1,k)) c= Seg (indx (D2,D1,(k + 1))) by A137, FINSEQ_1:5;
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 A216, FINSEQ_1:59 ;
then i in dom ((lower_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A221, A224, A223;
then A225: i in dom ((lower_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 16;
A226: ((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 16
.= (lower_volume (f,D2)) . i by A225, FUNCT_1:47 ;
A227: ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i = ((lower_volume (f,D2)) | (Seg (indx (D2,D1,k)))) . i by FINSEQ_1:def 16
.= (lower_volume (f,D2)) . i by A222, FUNCT_1:47 ;
i in dom p2 by A220, FINSEQ_1:def 3;
hence p2 . i = ((lower_volume (f,D2)) | (indx (D2,D1,k))) . i by A144, A227, A226, FINSEQ_1:def 7; :: thesis: verum
end;
then A228: p2 = (lower_volume (f,D2)) | (indx (D2,D1,k)) by A217, FINSEQ_1:14;
Sum ((lower_volume (f,D1)) | (k + 1)) = (Sum p1) + (Sum q1) by A112, RVSUM_1:75;
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 A148, XREAL_1:20;
then (Sum ((lower_volume (f,D1)) | (k + 1))) - (Sum q2) <= Sum p1 by XREAL_1:20;
then (Sum ((lower_volume (f,D1)) | (k + 1))) - (Sum q2) <= Sum p2 by A102, A131, A127, A228, 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 A215, XREAL_1:20; :: 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 zero Nat holds S1[n] from NAT_1:sch 10(A3, A101); :: thesis: verum
end;
hence for i being non zero 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