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_above holds
for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_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_above holds
for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
let f be Function of A,REAL; :: thesis: ( D1 <= D2 & f | A is bounded_above implies for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i))) )
assume that
A1: D1 <= D2 and
A2: f | A is bounded_above ; :: thesis: for i being non zero Element of NAT st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
for i being non zero Nat st i in dom D1 holds
Sum ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i)))
proof
defpred S1[ Nat] means ( $1 in dom D1 implies Sum ((upper_volume (f,D1)) | $1) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,$1))) );
A3: S1[1]
proof
reconsider g = f | (divset (D1,1)) as PartFunc of (divset (D1,1)),REAL by PARTFUN1:10;
set B = divset (D1,1);
set DD1 = mid (D1,1,1);
A4: dom g = (dom f) /\ (divset (D1,1)) by RELAT_1:61;
assume A5: 1 in dom D1 ; :: thesis: Sum ((upper_volume (f,D1)) | 1) >= Sum ((upper_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;
D1 . 1 >= lower_bound (divset (D1,1)) by A6, 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 (upper_volume (g,DD1)) = len DD1 by Def5
.= 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 (upper_volume (g,DD1)) holds
(upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (upper_volume (g,DD1)) implies (upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i )
assume that
A19: 1 <= i and
A20: i <= len (upper_volume (g,DD1)) ; :: thesis: (upper_volume (g,DD1)) . i = ((upper_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 (upper_volume (f,D1)) = Seg (len (upper_volume (f,D1))) by FINSEQ_1:def 3
.= Seg (len D1) by Def5 ;
then A23: dom ((upper_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: ((upper_volume (f,D1)) | 1) . i = ((upper_volume (f,D1)) | (Seg 1)) . i by FINSEQ_1:def 16
.= ((upper_volume (f,D1)) | (Seg 1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (upper_volume (f,D1)) . 1 by A23, FINSEQ_1:3, FUNCT_1:47
.= (upper_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) by A5, Def5 ;
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: (upper_volume (g,DD1)) . i = (upper_volume (g,DD1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (upper_bound (rng (g | (divset (DD1,1))))) * (vol (divset (DD1,1))) by A24, Def5 ;
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 (upper_volume (g,DD1)) . i = ((upper_volume (f,D1)) | 1) . i by A27, A26, A25; :: thesis: verum
end;
A28: g | (divset (D1,1)) is bounded_above
proof
consider a being Real such that
A29: for x being object st x in A /\ (dom f) holds
f . x <= a by A2, RFUNCT_1:70;
for x being object st x in (divset (D1,1)) /\ (dom g) holds
g . x <= a
proof
let x be object ; :: thesis: ( x in (divset (D1,1)) /\ (dom g) implies g . x <= a )
A30: dom g c= dom f by RELAT_1:60;
assume x in (divset (D1,1)) /\ (dom g) ; :: thesis: g . x <= a
then A31: x in dom g by XBOOLE_0:def 4;
A32: A /\ (dom f) = dom f by XBOOLE_1:28;
then x in A /\ (dom f) by A31, A30;
then reconsider x = x as Element of A ;
f . x <= a by A29, A31, A32, A30;
hence g . x <= a by A31, FUNCT_1:47; :: thesis: verum
end;
hence g | (divset (D1,1)) is bounded_above by RFUNCT_1:70; :: 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 (upper_volume (g,DD2)) holds
(upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (upper_volume (g,DD2)) implies (upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i )
assume that
A51: 1 <= i and
A52: i <= len (upper_volume (g,DD2)) ; :: thesis: (upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i
A53: i <= len DD2 by A52, Def5;
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: (upper_volume (g,DD2)) . i = (upper_bound (rng (g | (divset (D2,i))))) * (vol (divset (D2,i))) by A55, Def5;
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 A78: D2 . 1 <= D2 . (indx (D2,D1,1)) by A34, A36, SEQ_4:137;
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 upper_bound (divset (D2,i)) <= D1 . 1 by A1, A5, A78, Def18;
then A80: upper_bound (divset (D2,i)) <= upper_bound (divset (D1,1)) by A5, 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 ((upper_volume (f,D2)) | (Seg (indx (D2,D1,1)))) = (dom (upper_volume (f,D2))) /\ (Seg (indx (D2,D1,1))) by RELAT_1:61
.= (Seg (len (upper_volume (f,D2)))) /\ (Seg (indx (D2,D1,1))) by FINSEQ_1:def 3
.= (Seg (len D2)) /\ (Seg (indx (D2,D1,1))) by Def5
.= Seg (indx (D2,D1,1)) by A94, XBOOLE_1:28 ;
((upper_volume (f,D2)) | (indx (D2,D1,1))) . i = ((upper_volume (f,D2)) | (Seg (indx (D2,D1,1)))) . i by FINSEQ_1:def 16
.= (upper_volume (f,D2)) . i by A43, A54, A97, FUNCT_1:47
.= (upper_bound (rng (f | (divset (D2,i))))) * (vol (divset (D2,i))) by A95, Def5 ;
hence (upper_volume (g,DD2)) . i = ((upper_volume (f,D2)) | (indx (D2,D1,1))) . i by A72, A96, FUNCT_1:51; :: thesis: verum
end;
len (upper_volume (g,DD1)) = len ((upper_volume (f,D1)) | 1) by A10;
then A98: upper_volume (g,DD1) = (upper_volume (f,D1)) | 1 by A18, FINSEQ_1:14;
A99: indx (D2,D1,1) <= len (upper_volume (f,D2)) by A41, Def5;
len (upper_volume (g,DD2)) = indx (D2,D1,1) by A43, Def5;
then A100: len (upper_volume (g,DD2)) = len ((upper_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 upper_sum (g,DD1) >= upper_sum (g,DD2) by A11, A28, Th28;
hence Sum ((upper_volume (f,D1)) | 1) >= Sum ((upper_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 ((upper_volume (f,D1)) | k) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,k))) ) ; :: thesis: S1[k + 1]
assume A103: k + 1 in dom D1 ; :: thesis: Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_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 ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
per cases ( 1 = k + 1 or 1 <> k + 1 ) ;
suppose 1 = k + 1 ; :: thesis: Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
hence Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A3, A103; :: thesis: verum
end;
suppose A107: 1 <> k + 1 ; :: thesis: Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))
set IDK = indx (D2,D1,k);
set IDK1 = indx (D2,D1,(k + 1));
set K1D2 = (upper_volume (f,D2)) | (indx (D2,D1,(k + 1)));
set KD1 = (upper_volume (f,D1)) | k;
set K1D1 = (upper_volume (f,D1)) | (k + 1);
set n = k + 1;
A108: k + 1 <= len (upper_volume (f,D1)) by A106, Def5;
then A109: len ((upper_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: (upper_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 (upper_volume (f,D1)) by Def5;
then A116: len p1 = len ((upper_volume (f,D1)) | k) by A110, FINSEQ_1:59;
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = ((upper_volume (f,D1)) | k) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len p1 implies p1 . i = ((upper_volume (f,D1)) | k) . i )
assume that
A117: 1 <= i and
A118: i <= len p1 ; :: thesis: p1 . i = ((upper_volume (f,D1)) | k) . i
A119: i in Seg (len p1) by A117, A118, FINSEQ_1:1;
then A120: i in dom ((upper_volume (f,D1)) | k) by A116, FINSEQ_1:def 3;
then A121: i in dom ((upper_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 ((upper_volume (f,D1)) | (k + 1)) = Seg (len ((upper_volume (f,D1)) | (k + 1))) by FINSEQ_1:def 3
.= Seg (k + 1) by A108, FINSEQ_1:59 ;
dom ((upper_volume (f,D1)) | k) = Seg (len ((upper_volume (f,D1)) | k)) by FINSEQ_1:def 3
.= Seg k by A115, FINSEQ_1:59 ;
then i in dom ((upper_volume (f,D1)) | (k + 1)) by A120, A122, A123;
then A124: i in dom ((upper_volume (f,D1)) | (Seg (k + 1))) by FINSEQ_1:def 16;
A125: ((upper_volume (f,D1)) | (k + 1)) . i = ((upper_volume (f,D1)) | (Seg (k + 1))) . i by FINSEQ_1:def 16
.= (upper_volume (f,D1)) . i by A124, FUNCT_1:47 ;
A126: ((upper_volume (f,D1)) | k) . i = ((upper_volume (f,D1)) | (Seg k)) . i by FINSEQ_1:def 16
.= (upper_volume (f,D1)) . i by A121, FUNCT_1:47 ;
i in dom p1 by A119, FINSEQ_1:def 3;
hence p1 . i = ((upper_volume (f,D1)) | k) . i by A112, A126, A125, FINSEQ_1:def 7; :: thesis: verum
end;
then A127: p1 = (upper_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 (upper_volume (f,D2)) = len D2 by Def5;
then A141: indx (D2,D1,(k + 1)) <= len (upper_volume (f,D2)) by A129, FINSEQ_1:1;
then len ((upper_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: (upper_volume (f,D2)) | (indx (D2,D1,(k + 1))) = p2 ^ q2 by A139, FINSEQ_2:23;
indx (D2,D1,k) in dom D2 by A1, A132, Def18;
then A145: indx (D2,D1,k) in Seg (len (upper_volume (f,D2))) by A140, FINSEQ_1:def 3;
then A146: 1 <= indx (D2,D1,k) by FINSEQ_1:1;
set KD2 = (upper_volume (f,D2)) | (indx (D2,D1,k));
A147: Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = (Sum p2) + (Sum q2) by A144, RVSUM_1:75;
A148: indx (D2,D1,k) <= len (upper_volume (f,D2)) by A145, FINSEQ_1:1;
then A149: len p2 = len ((upper_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 = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len p2 implies p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i )
assume that
A150: 1 <= i and
A151: i <= len p2 ; :: thesis: p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i
A152: i in Seg (len p2) by A150, A151, FINSEQ_1:1;
then A153: i in dom ((upper_volume (f,D2)) | (indx (D2,D1,k))) by A149, FINSEQ_1:def 3;
then A154: i in dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,k)))) by FINSEQ_1:def 16;
A155: dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = Seg (len ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 3
.= Seg (indx (D2,D1,(k + 1))) by A141, FINSEQ_1:59 ;
A156: Seg (indx (D2,D1,k)) c= Seg (indx (D2,D1,(k + 1))) by A137, FINSEQ_1:5;
dom ((upper_volume (f,D2)) | (indx (D2,D1,k))) = Seg (len ((upper_volume (f,D2)) | (indx (D2,D1,k)))) by FINSEQ_1:def 3
.= Seg (indx (D2,D1,k)) by A148, FINSEQ_1:59 ;
then i in dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A153, A156, A155;
then A157: i in dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 16;
A158: ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . i = ((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . i by FINSEQ_1:def 16
.= (upper_volume (f,D2)) . i by A157, FUNCT_1:47 ;
A159: ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i = ((upper_volume (f,D2)) | (Seg (indx (D2,D1,k)))) . i by FINSEQ_1:def 16
.= (upper_volume (f,D2)) . i by A154, FUNCT_1:47 ;
i in dom p2 by A152, FINSEQ_1:def 3;
hence p2 . i = ((upper_volume (f,D2)) | (indx (D2,D1,k))) . i by A144, A159, A158, FINSEQ_1:def 7; :: thesis: verum
end;
then A160: p2 = (upper_volume (f,D2)) | (indx (D2,D1,k)) by A149, FINSEQ_1:14;
A161: indx (D2,D1,(k + 1)) <= len D2 by A129, FINSEQ_1:1;
A162: ID = (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) by A139;
A163: 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)));
A164: 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 A165: lower_bound (divset (D1,(k + 1))) = D1 . k by A103, A107, Def3;
D2 . (indx (D2,D1,(k + 1))) = D1 . (k + 1) by A1, A103, Def18;
then A166: D2 . (indx (D2,D1,(k + 1))) = upper_bound (divset (D1,(k + 1))) by A103, A107, Def3;
A167: (indx (D2,D1,k)) + 1 <= indx (D2,D1,(k + 1)) by A134, NAT_1:13;
then A168: (indx (D2,D1,k)) + 1 <= len D2 by A161, XXREAL_0:2;
then (indx (D2,D1,k)) + 1 in Seg (len D2) by A164, FINSEQ_1:1;
then A169: (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, A165, 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, A167, A169, A166, Th35;
A170: ((indx (D2,D1,(k + 1))) -' ((indx (D2,D1,k)) + 1)) + 1 = ((indx (D2,D1,(k + 1))) - ((indx (D2,D1,k)) + 1)) + 1 by A167, XREAL_1:233
.= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) ;
A171: for n being Nat st 1 <= n & n <= len q2 holds
q2 . n = (upper_volume (g,MD2)) . n
proof
A172: dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) = Seg (len ((upper_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 A173: dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) c= Seg (len D2) by A161, FINSEQ_1:5;
then A174: dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) c= dom D2 by FINSEQ_1:def 3;
A175: len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) = ID by A130, A161, A139, A167, A168, A164, A170, FINSEQ_6:118;
let n be Nat; :: thesis: ( 1 <= n & n <= len q2 implies q2 . n = (upper_volume (g,MD2)) . n )
assume that
A176: 1 <= n and
A177: n <= len q2 ; :: thesis: q2 . n = (upper_volume (g,MD2)) . n
n in Seg (len q2) by A176, A177, FINSEQ_1:1;
then A178: n in dom q2 by FINSEQ_1:def 3;
then A179: (indx (D2,D1,k)) + n in dom ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A142, A144, FINSEQ_1:28;
then A180: (indx (D2,D1,k)) + n in dom ((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) by FINSEQ_1:def 16;
A181: q2 . n = ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) . ((indx (D2,D1,k)) + n) by A142, A144, A178, FINSEQ_1:def 7
.= ((upper_volume (f,D2)) | (Seg (indx (D2,D1,(k + 1))))) . ((indx (D2,D1,k)) + n) by FINSEQ_1:def 16
.= (upper_volume (f,D2)) . ((indx (D2,D1,k)) + n) by A180, FUNCT_1:47
.= (upper_bound (rng (f | (divset (D2,((indx (D2,D1,k)) + n)))))) * (vol (divset (D2,((indx (D2,D1,k)) + n)))) by A179, A174, Def5 ;
(indx (D2,D1,k)) + n in Seg (len D2) by A179, A173;
then A182: (indx (D2,D1,k)) + n in dom D2 by FINSEQ_1:def 3;
(indx (D2,D1,k)) + n <= indx (D2,D1,(k + 1)) by A172, A179, FINSEQ_1:1;
then A183: n <= ID by A162, XREAL_1:19;
then n in Seg ID by A176, FINSEQ_1:1;
then A184: n in dom MD2 by A175, FINSEQ_1:def 3;
n in Seg (len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1)))))) by A176, A183, A175, FINSEQ_1:1;
then A185: n in dom (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) by FINSEQ_1:def 3;
A186: 1 <= (indx (D2,D1,k)) + n by A172, A179, FINSEQ_1:1;
A187: ( 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 A188: 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 A189: (indx (D2,D1,k)) + 1 <= len D2 by A179, A173, FINSEQ_1:1;
A190: 1 <= (indx (D2,D1,k)) + 1 by A172, A179, A188, FINSEQ_1:1;
A191: upper_bound (divset (MD2,1)) = (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) . 1 by A184, A188, Def3
.= D2 . (1 + (indx (D2,D1,k))) by A130, A161, A190, A189, FINSEQ_6:118 ;
A192: (indx (D2,D1,k)) + 1 <> 1 by A146, NAT_1:13;
A193: (k + 1) - 1 = k ;
A194: lower_bound (divset (MD2,1)) = lower_bound (divset (D1,(k + 1))) by A184, A188, Def3
.= D1 . k by A103, A107, A193, Def3 ;
A195: 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 A188, Th2
.= [.(D2 . (((indx (D2,D1,k)) + 1) - 1)),(upper_bound (divset (D2,((indx (D2,D1,k)) + 1)))).] by A169, A192, Def3
.= [.(D2 . (indx (D2,D1,k))),(D2 . ((indx (D2,D1,k)) + 1)).] by A169, A192, 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 A188, A194, A191, 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 A188, A194, 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 A184, A195, Th6; :: thesis: verum
end;
suppose A196: 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)) )
A197: (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 A146, XREAL_1:19;
then n <= 1 - 1 by XREAL_1:19;
hence contradiction by A176, NAT_1:3; :: thesis: verum
end;
A198: 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 A182, A197, Def3
.= [.(D2 . (((indx (D2,D1,k)) + n) - 1)),(D2 . ((indx (D2,D1,k)) + n)).] by A182, A197, Def3 ;
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:20;
then A199: n - 1 <= len MD2 by A183, A175, XXREAL_0:2;
consider n1 being Nat such that
A200: n = 1 + n1 by A176, NAT_1:10;
not n is trivial by A176, A196, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:29;
then A201: 1 <= n - 1 by XREAL_1:19;
A202: (indx (D2,D1,k)) + 1 <= indx (D2,D1,(k + 1)) by A134, NAT_1:13;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 12;
A203: (n1 + ((indx (D2,D1,k)) + 1)) -' 1 = ((indx (D2,D1,k)) + n) - 1 by A186, A200, XREAL_1:233;
A204: (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 ;
A205: lower_bound (divset (MD2,n)) = MD2 . (n - 1) by A184, A196, Def3
.= D2 . (((indx (D2,D1,k)) + n) - 1) by A130, A161, A168, A164, A202, A200, A203, A201, A199, FINSEQ_6:118 ;
A206: upper_bound (divset (MD2,n)) = MD2 . n by A184, A196, Def3
.= D2 . ((indx (D2,D1,k)) + n) by A130, A161, A168, A164, A176, A183, A175, A202, A204, FINSEQ_6:118 ;
hence divset (MD2,n) = divset (D2,((indx (D2,D1,k)) + n)) by A205, A198, 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 A205, A206, 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 A184, A198, 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 = (upper_volume (g,MD2)) . n by A185, A181, A187, Def5; :: thesis: verum
end;
(k + 1) - 1 = k ;
then A207: 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, A207, Th35, SEQ_4:137;
A208: g | (divset (D1,(k + 1))) is bounded_above
proof
consider a being Real such that
A209: for x being object st x in A /\ (dom f) holds
f . x <= a by A2, RFUNCT_1:70;
for x being object st x in (divset (D1,(k + 1))) /\ (dom g) holds
g . x <= a
proof
let x be object ; :: thesis: ( x in (divset (D1,(k + 1))) /\ (dom g) implies g . x <= a )
A210: dom g c= dom f by RELAT_1:60;
assume x in (divset (D1,(k + 1))) /\ (dom g) ; :: thesis: g . x <= a
then A211: x in dom g by XBOOLE_0:def 4;
A212: A /\ (dom f) = dom f by XBOOLE_1:28;
then x in A /\ (dom f) by A211, A210;
then reconsider x = x as Element of A ;
f . x <= a by A209, A211, A212, A210;
hence g . x <= a by A211, FUNCT_1:47; :: thesis: verum
end;
hence g | (divset (D1,(k + 1))) is bounded_above by RFUNCT_1:70; :: thesis: verum
end;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A105, A106, FINSEQ_6:118;
then A213: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:233;
then A214: dom q1 = dom MD1 by A111, FINSEQ_3:29;
A215: for n being Nat st 1 <= n & n <= len q1 holds
q1 . n = (upper_volume (g,MD1)) . n
proof
k + 1 in Seg (len ((upper_volume (f,D1)) | (k + 1))) by A109, FINSEQ_1:4;
then k + 1 in dom ((upper_volume (f,D1)) | (k + 1)) by FINSEQ_1:def 3;
then A216: k + 1 in dom ((upper_volume (f,D1)) | (Seg (k + 1))) by FINSEQ_1:def 16;
A217: MD1 . 1 = D1 . (k + 1) by A105, A106, FINSEQ_6:118;
1 in Seg (len MD1) by A213, FINSEQ_1:3;
then A218: 1 in dom MD1 by FINSEQ_1:def 3;
divset (MD1,1) = [.(lower_bound (divset (MD1,1))),(upper_bound (divset (MD1,1))).] by Th2;
then A219: divset (MD1,1) = [.(lower_bound (divset (D1,(k + 1)))),(upper_bound (divset (MD1,1))).] by A218, Def3
.= [.(lower_bound (divset (D1,(k + 1)))),(D1 . (k + 1)).] by A218, A217, Def3 ;
(k + 1) - 1 = k ;
then A220: lower_bound (divset (D1,(k + 1))) = D1 . k by A103, A107, Def3;
let n be Nat; :: thesis: ( 1 <= n & n <= len q1 implies q1 . n = (upper_volume (g,MD1)) . n )
assume that
A221: 1 <= n and
A222: n <= len q1 ; :: thesis: q1 . n = (upper_volume (g,MD1)) . n
A223: n = 1 by A111, A221, A222, XXREAL_0:1;
n in Seg (len q1) by A221, A222, FINSEQ_1:1;
then A224: n in dom q1 by FINSEQ_1:def 3;
upper_bound (divset (D1,(k + 1))) = D1 . (k + 1) by A103, A107, Def3;
then divset (D1,(k + 1)) = [.(D1 . k),(D1 . (k + 1)).] by A220, Th2;
then A225: (upper_volume (g,MD1)) . n = (upper_bound (rng (g | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1)))) by A214, A223, A224, A219, A220, Def5;
((upper_volume (f,D1)) | (k + 1)) . (k + 1) = ((upper_volume (f,D1)) | (Seg (k + 1))) . (k + 1) by FINSEQ_1:def 16
.= (upper_volume (f,D1)) . (k + 1) by A216, FUNCT_1:47 ;
then q1 . n = (upper_volume (f,D1)) . (k + 1) by A110, A112, A223, A224, FINSEQ_1:def 7
.= (upper_bound (rng (f | (divset (D1,(k + 1)))))) * (vol (divset (D1,(k + 1)))) by A103, Def5 ;
hence q1 . n = (upper_volume (g,MD1)) . n by A225; :: thesis: verum
end;
len q1 = len (upper_volume (g,MD1)) by A111, A213, Def5;
then A226: q1 = upper_volume (g,MD1) by A215, FINSEQ_1:14;
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 A227: g is total by PARTFUN1:def 2;
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 A228: upper_sum (g,MD1) >= upper_sum (g,MD2) by A208, A227, Th28;
len (upper_volume (g,MD2)) = len (mid (D2,((indx (D2,D1,k)) + 1),(indx (D2,D1,(k + 1))))) by Def5
.= (indx (D2,D1,(k + 1))) - (indx (D2,D1,k)) by A130, A161, A167, A168, A164, A170, FINSEQ_6:118 ;
hence Sum q1 >= Sum q2 by A143, A226, A171, A228, FINSEQ_1:14; :: thesis: verum
end;
Sum ((upper_volume (f,D1)) | (k + 1)) = (Sum p1) + (Sum q1) by A112, RVSUM_1:75;
then Sum q1 = (Sum ((upper_volume (f,D1)) | (k + 1))) - (Sum p1) ;
then Sum ((upper_volume (f,D1)) | (k + 1)) >= (Sum q2) + (Sum p1) by A163, XREAL_1:19;
then (Sum ((upper_volume (f,D1)) | (k + 1))) - (Sum q2) >= Sum p1 by XREAL_1:19;
then (Sum ((upper_volume (f,D1)) | (k + 1))) - (Sum q2) >= Sum p2 by A102, A131, A127, A160, FINSEQ_1:def 3, XXREAL_0:2;
hence Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) by A147, XREAL_1:19; :: thesis: verum
end;
end;
end;
hence Sum ((upper_volume (f,D1)) | (k + 1)) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,(k + 1)))) ; :: thesis: verum
end;
thus for k being non zero Nat holds S1[k] 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 ((upper_volume (f,D1)) | i) >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i))) ; :: thesis: verum