proof

let k be non empty Nat; :: thesis:
assume A93: ( k in dom D1 implies Sum ((upper_volume f,D1) | k) >= Sum ((upper_volume f,D2) | (indx D2,D1,k)) ) ; :: thesis:
assume A94: k + 1 in dom D1 ; :: thesis:
then k + 1 in Seg (len D1) by FINSEQ_1:def 3;
then A96: ( 1 <= k + 1 & k + 1 <= len D1 ) by FINSEQ_1:3;

now

per cases ;

suppose 1 = k + 1 ; :: thesis:

hence Sum ((upper_volume f,D1) | (k + 1)) >= Sum ((upper_volume f,D2) | (indx D2,D1,(k + 1))) by A3, A94; :: thesis:

end;

suppose A97: 1 <> k + 1 ; :: thesis:

set n = k + 1;
not k + 1 is trivial by A97, NAT_2:def 1;
then k + 1 >= 2 by NAT_2:31;
then A98: k >= (1 + 1) - 1 by XREAL_1:22;
A99: k <= k + 1 by NAT_1:11;
then A100: ( 1 <= k & k <= len D1 ) by A96, A98, XXREAL_0:2;
then A101: k in Seg (len D1) by FINSEQ_1:3;
then A102: k in dom D1 by FINSEQ_1:def 3;
A103: ( 1 <= k + 1 & k + 1 <= len (upper_volume f,D1) ) by A96, Def7;
A104: len (upper_volume f,D2) = len D2 by Def7;
A105: indx D2,D1,k in dom D2 by A1, A102, Def21;
A106: indx D2,D1,(k + 1) in dom D2 by A1, A94, Def21;
then A107: indx D2,D1,(k + 1) in Seg (len D2) by FINSEQ_1:def 3;
then A108: ( 1 <= indx D2,D1,(k + 1) & indx D2,D1,(k + 1) <= len D2 ) by FINSEQ_1:3;
A109: ( 1 <= indx D2,D1,(k + 1) & indx D2,D1,(k + 1) <= len (upper_volume f,D2) ) by A104, A107, FINSEQ_1:3;
A110: indx D2,D1,k < indx D2,D1,(k + 1)

proof

assume indx D2,D1,k >= indx D2,D1,(k + 1) ; :: thesis:
then A111: D2 . (indx D2,D1,k) >= D2 . (indx D2,D1,(k + 1)) by A105, A106, GOBOARD2:18;
k < k + 1 by NAT_1:13;
then A112: D1 . k < D1 . (k + 1) by A94, A102, SEQM_3:def 1;
D1 . k = D2 . (indx D2,D1,k) by A1, A102, Def21;
hence contradiction by A1, A94, A111, A112, Def21; :: thesis:

end;

A113: indx D2,D1,(k + 1) >= indx D2,D1,k

proof

assume indx D2,D1,(k + 1) < indx D2,D1,k ; :: thesis:
then A114: D2 . (indx D2,D1,(k + 1)) < D2 . (indx D2,D1,k) by A105, A106, SEQM_3:def 1;
D1 . (k + 1) = D2 . (indx D2,D1,(k + 1)) by A1, A94, Def21;
then D1 . (k + 1) < D1 . k by A1, A102, A114, Def21;
hence contradiction by A94, A102, GOBOARD2:18, NAT_1:11; :: thesis:

end;

then consider ID being Nat such that
A115: 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;
A116: ID = (indx D2,D1,(k + 1)) - (indx D2,D1,k) by A115;
A117: ( 1 <= k & k <= len (upper_volume f,D1) ) by A100, Def7;
indx D2,D1,k in dom D2 by A1, A102, Def21;
then indx D2,D1,k in Seg (len (upper_volume f,D2)) by A104, FINSEQ_1:def 3;
then A118: ( 1 <= indx D2,D1,k & indx D2,D1,k <= len (upper_volume f,D2) ) by FINSEQ_1:3;
set K1D1 = (upper_volume f,D1) | (k + 1);
set KD1 = (upper_volume f,D1) | k;
set K1D2 = (upper_volume f,D2) | (indx D2,D1,(k + 1));
set KD2 = (upper_volume f,D2) | (indx D2,D1,k);
set IDK1 = indx D2,D1,(k + 1);
set IDK = indx D2,D1,k;
A119: len ((upper_volume f,D1) | (k + 1)) = k + 1 by A103, FINSEQ_1:80;
then consider p1, q1 being FinSequence of REAL such that
A120: ( len p1 = k & len q1 = 1 & (upper_volume f,D1) | (k + 1) = p1 ^ q1 ) by FINSEQ_2:26;
len ((upper_volume f,D2) | (indx D2,D1,(k + 1))) = (indx D2,D1,k) + ((indx D2,D1,(k + 1)) - (indx D2,D1,k)) by A109, FINSEQ_1:80;
then consider p2, q2 being FinSequence of REAL such that
A121: ( len p2 = indx D2,D1,k & len q2 = (indx D2,D1,(k + 1)) - (indx D2,D1,k) & (upper_volume f,D2) | (indx D2,D1,(k + 1)) = p2 ^ q2 ) by A115, FINSEQ_2:26;
A122: p1 = (upper_volume f,D1) | k

proof

A123: len p1 = len ((upper_volume f,D1) | k) by A117, A120, FINSEQ_1:80;
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:
assume ( 1 <= i & i <= len p1 ) ; :: thesis:
then A124: i in Seg (len p1) by FINSEQ_1:3;
then A125: i in dom p1 by FINSEQ_1:def 3;
A126: i in dom ((upper_volume f,D1) | k) by A123, A124, FINSEQ_1:def 3;
then A127: i in dom ((upper_volume f,D1) | (Seg k)) by FINSEQ_1:def 15;
A128: ((upper_volume f,D1) | k) . i = ((upper_volume f,D1) | (Seg k)) . i by FINSEQ_1:def 15
.= (upper_volume f,D1) . i by A127, FUNCT_1:70 ;
A129: dom ((upper_volume f,D1) | k) = Seg (len ((upper_volume f,D1) | k)) by FINSEQ_1:def 3
.= Seg k by A117, FINSEQ_1:80 ;
k <= k + 1 by NAT_1:11;
then A130: Seg k c= Seg (k + 1) by FINSEQ_1:7;
dom ((upper_volume f,D1) | (k + 1)) = Seg (len ((upper_volume f,D1) | (k + 1))) by FINSEQ_1:def 3
.= Seg (k + 1) by A103, FINSEQ_1:80 ;
then i in dom ((upper_volume f,D1) | (k + 1)) by A126, A129, A130;
then A131: i in dom ((upper_volume f,D1) | (Seg (k + 1))) by FINSEQ_1:def 15;
((upper_volume f,D1) | (k + 1)) . i = ((upper_volume f,D1) | (Seg (k + 1))) . i by FINSEQ_1:def 15
.= (upper_volume f,D1) . i by A131, FUNCT_1:70 ;
hence p1 . i = ((upper_volume f,D1) | k) . i by A120, A125, A128, FINSEQ_1:def 7; :: thesis:

end;

hence p1 = (upper_volume f,D1) | k by A123, FINSEQ_1:18; :: thesis:

end;

A132: p2 = (upper_volume f,D2) | (indx D2,D1,k)

proof

A133: len p2 = len ((upper_volume f,D2) | (indx D2,D1,k)) by A118, A121, FINSEQ_1:80;
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:
assume ( 1 <= i & i <= len p2 ) ; :: thesis:
then A134: i in Seg (len p2) by FINSEQ_1:3;
then A135: i in dom p2 by FINSEQ_1:def 3;
A136: i in dom ((upper_volume f,D2) | (indx D2,D1,k)) by A133, A134, FINSEQ_1:def 3;
then A137: i in dom ((upper_volume f,D2) | (Seg (indx D2,D1,k))) by FINSEQ_1:def 15;
A138: ((upper_volume f,D2) | (indx D2,D1,k)) . i = ((upper_volume f,D2) | (Seg (indx D2,D1,k))) . i by FINSEQ_1:def 15
.= (upper_volume f,D2) . i by A137, FUNCT_1:70 ;
A139: 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 A118, FINSEQ_1:80 ;
A140: Seg (indx D2,D1,k) c= Seg (indx D2,D1,(k + 1)) by A113, FINSEQ_1:7;
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 A109, FINSEQ_1:80 ;
then i in dom ((upper_volume f,D2) | (indx D2,D1,(k + 1))) by A136, A139, A140;
then A141: i in dom ((upper_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
((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 15
.= (upper_volume f,D2) . i by A141, FUNCT_1:70 ;
hence p2 . i = ((upper_volume f,D2) | (indx D2,D1,k)) . i by A121, A135, A138, FINSEQ_1:def 7; :: thesis:

end;

hence p2 = (upper_volume f,D2) | (indx D2,D1,k) by A133, FINSEQ_1:18; :: thesis:

end;

A142: Sum q1 >= Sum q2

proof

set DD1 = divset D1,(k + 1);
set MD1 = mid D1,(k + 1),(k + 1);
set MD2 = mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1));
set g = f | (divset D1,(k + 1));
set S1 = divs (divset D1,(k + 1));
A143: ( k + 1 in dom D1 & D1 . (k + 1) >= lower_bound (divset D1,(k + 1)) & D1 . (k + 1) = upper_bound (divset D1,(k + 1)) )

proof

(k + 1) - 1 = k ;
then lower_bound (divset D1,(k + 1)) = D1 . k by A94, A97, Def5;
hence ( k + 1 in dom D1 & D1 . (k + 1) >= lower_bound (divset D1,(k + 1)) & D1 . (k + 1) = upper_bound (divset D1,(k + 1)) ) by A94, A97, A99, A102, Def5, GOBOARD2:18; :: thesis:

end;

then reconsider MD1 = mid D1,(k + 1),(k + 1) as Division of divset D1,(k + 1) by Th39;
A144: (indx D2,D1,k) + 1 <= indx D2,D1,(k + 1) by A110, NAT_1:13;
then A145: (indx D2,D1,k) + 1 <= len D2 by A108, XXREAL_0:2;
A146: 1 <= (indx D2,D1,k) + 1 by NAT_1:11;
then (indx D2,D1,k) + 1 in Seg (len D2) by A145, FINSEQ_1:3;
then A147: (indx D2,D1,k) + 1 in dom D2 by FINSEQ_1:def 3;
A148: D2 . (indx D2,D1,(k + 1)) = D1 . (k + 1) by A1, A94, Def21;
(k + 1) - 1 = k ;
then A149: lower_bound (divset D1,(k + 1)) = D1 . k by A94, A97, Def5;
D2 . ((indx D2,D1,k) + 1) >= D2 . (indx D2,D1,k) by A105, A147, GOBOARD2:18, NAT_1:11;
then A150: D2 . ((indx D2,D1,k) + 1) >= lower_bound (divset D1,(k + 1)) by A1, A102, A149, Def21;
D2 . (indx D2,D1,(k + 1)) = upper_bound (divset D1,(k + 1)) by A94, A97, A148, Def5;
then reconsider MD2 = mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1)) as Division of divset D1,(k + 1) by A106, A144, A147, A150, Th39;
reconsider g = f | (divset D1,(k + 1)) as PartFunc of (divset D1,(k + 1)),REAL by PARTFUN1:43;
A151: ( g is total & g | (divset D1,(k + 1)) is bounded_above )

proof

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 A143, Th10, XBOOLE_1:28;
hence g is total by PARTFUN1:def 4; :: thesis:
g | (divset D1,(k + 1)) is bounded_above

proof

consider a being real number such that
A152: for x being set st x in A /\ (dom f) holds
f . x <= a by A2, RFUNCT_1:87;
for x being set st x in (divset D1,(k + 1)) /\ (dom g) holds
g . x <= a

proof

let x be set ; :: thesis:
assume x in (divset D1,(k + 1)) /\ (dom g) ; :: thesis:
then A153: x in dom g by XBOOLE_0:def 4;
A154: A /\ (dom f) = dom f by XBOOLE_1:28;
A155: dom g c= dom f by RELAT_1:89;
then x in A /\ (dom f) by A153, A154;
then reconsider x = x as Element of A ;
f . x <= a by A152, A153, A154, A155;
hence g . x <= a by A153, FUNCT_1:70; :: thesis:

end;

hence g | (divset D1,(k + 1)) is bounded_above by RFUNCT_1:87; :: thesis:

end;

hence g | (divset D1,(k + 1)) is bounded_above ; :: thesis:

end;

A157: q1 = upper_volume g,MD1

proof

len MD1 = ((k + 1) -' (k + 1)) + 1 by A96, JORDAN3:27;
then A158: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
then A159: len q1 = len (upper_volume g,MD1) by A120, Def7;
Y: dom q1 = dom MD1 by A120, A158, FINSEQ_3:31;
for n being Nat st 1 <= n & n <= len q1 holds
q1 . n = (upper_volume g,MD1) . n

proof

let n be Nat; :: thesis:
assume A160: ( 1 <= n & n <= len q1 ) ; :: thesis:
then A161: n = 1 by A120, XXREAL_0:1;
n in Seg (len q1) by A160, FINSEQ_1:3;
then A163: n in dom q1 by FINSEQ_1:def 3;
k + 1 in Seg (len ((upper_volume f,D1) | (k + 1))) by A119, FINSEQ_1:6;
then k + 1 in dom ((upper_volume f,D1) | (k + 1)) by FINSEQ_1:def 3;
then A164: k + 1 in dom ((upper_volume f,D1) | (Seg (k + 1))) by FINSEQ_1:def 15;
((upper_volume f,D1) | (k + 1)) . (k + 1) = ((upper_volume f,D1) | (Seg (k + 1))) . (k + 1) by FINSEQ_1:def 15
.= (upper_volume f,D1) . (k + 1) by A164, FUNCT_1:70 ;
then A165: q1 . n = (upper_volume f,D1) . (k + 1) by A120, A161, A163, FINSEQ_1:def 7
.= (upper_bound (rng (f | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by Def7, A94 ;
A166: divset MD1,1 = [.(lower_bound (divset MD1,1)),(upper_bound (divset MD1,1)).] by Th5;
A167: 1 in dom MD1

proof

1 in Seg (len MD1) by A158, FINSEQ_1:5;
hence 1 in dom MD1 by FINSEQ_1:def 3; :: thesis:

end;

A168: MD1 . 1 = D1 . (k + 1) by A96, JORDAN3:27;
A169: divset MD1,1 = [.(lower_bound (divset D1,(k + 1))),(upper_bound (divset MD1,1)).] by A166, A167, Def5
.= [.(lower_bound (divset D1,(k + 1))),(D1 . (k + 1)).] by A167, A168, Def5 ;
(k + 1) - 1 = k ;
then A170: lower_bound (divset D1,(k + 1)) = D1 . k by A94, A97, Def5;
upper_bound (divset D1,(k + 1)) = D1 . (k + 1) by A94, A97, Def5;
then divset D1,(k + 1) = [.(D1 . k),(D1 . (k + 1)).] by A170, Th5;
then (upper_volume g,MD1) . n = (upper_bound (rng (g | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by A161, A169, A170, Def7, A163, Y;
hence q1 . n = (upper_volume g,MD1) . n by A165, FUNCT_1:82; :: thesis:

end;

hence q1 = upper_volume g,MD1 by A159, FINSEQ_1:18; :: thesis:

end;

A171: q2 = upper_volume g,MD2

proof

A172: ((indx D2,D1,(k + 1)) -' ((indx D2,D1,k) + 1)) + 1 = ((indx D2,D1,(k + 1)) - ((indx D2,D1,k) + 1)) + 1 by A144, XREAL_1:235
.= (indx D2,D1,(k + 1)) - (indx D2,D1,k) ;
A173: len (upper_volume g,MD2) = len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) by Def7
.= (indx D2,D1,(k + 1)) - (indx D2,D1,k) by A108, A144, A145, A146, A172, JORDAN3:27 ;
for n being Nat st 1 <= n & n <= len q2 holds
q2 . n = (upper_volume g,MD2) . n

proof

let n be Nat; :: thesis:
assume A174: ( 1 <= n & n <= len q2 ) ; :: thesis:
then A175: n in Seg (len q2) by FINSEQ_1:3;
then A176: n in dom q2 by FINSEQ_1:def 3;
A177: 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 A109, FINSEQ_1:80 ;
A178: (indx D2,D1,k) + n in dom ((upper_volume f,D2) | (indx D2,D1,(k + 1))) by A121, A176, FINSEQ_1:41;
then A179: (indx D2,D1,k) + n in dom ((upper_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
A180: dom ((upper_volume f,D2) | (indx D2,D1,(k + 1))) c= Seg (len D2) by A108, A177, FINSEQ_1:7;
then B180: dom ((upper_volume f,D2) | (indx D2,D1,(k + 1))) c= dom D2 by FINSEQ_1:def 3;
(indx D2,D1,k) + n in Seg (len D2) by A178, A180;
then A181: (indx D2,D1,k) + n in dom D2 by FINSEQ_1:def 3;
A182: ( 1 <= (indx D2,D1,k) + n & (indx D2,D1,k) + n <= indx D2,D1,(k + 1) ) by A177, A178, FINSEQ_1:3;
then A183: n <= ID by A116, XREAL_1:21;
then A184: n in Seg ID by A174, FINSEQ_1:3;
A185: len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) = ID by A108, A115, A144, A145, A146, A172, JORDAN3:27;
then n in Seg (len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1)))) by A174, A183, FINSEQ_1:3;
then B186: n in dom (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) by FINSEQ_1:def 3;
A187: n in dom MD2 by A184, A185, FINSEQ_1:def 3;
A188: q2 . n = ((upper_volume f,D2) | (indx D2,D1,(k + 1))) . ((indx D2,D1,k) + n) by A121, A176, FINSEQ_1:def 7
.= ((upper_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) . ((indx D2,D1,k) + n) by FINSEQ_1:def 15
.= (upper_volume f,D2) . ((indx D2,D1,k) + n) by A179, FUNCT_1:70
.= (upper_bound (rng (f | (divset D2,((indx D2,D1,k) + n))))) * (vol (divset D2,((indx D2,D1,k) + n))) by A178, Def7, B180 ;
A189: ( 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 ;

suppose A190: n = 1 ; :: thesis:

A191: (k + 1) - 1 = k ;
A192: ( 1 <= (indx D2,D1,k) + 1 & (indx D2,D1,k) + 1 <= len D2 ) by A178, A180, A190, FINSEQ_1:3;
A193: (indx D2,D1,k) + 1 <> 1 by A118, NAT_1:13;
A194: lower_bound (divset MD2,1) = lower_bound (divset D1,(k + 1)) by A187, A190, Def5
.= D1 . k by A94, A97, A191, Def5 ;
A195: upper_bound (divset MD2,1) = (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) . 1 by A187, A190, Def5
.= D2 . (1 + (indx D2,D1,k)) by A108, A192, JORDAN3:27 ;
then A196: divset MD2,n = [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A190, A194, Th5;
A197: 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 A190, Th5
.= [.(D2 . (((indx D2,D1,k) + 1) - 1)),(upper_bound (divset D2,((indx D2,D1,k) + 1))).] by A147, A193, Def5
.= [.(D2 . (indx D2,D1,k)),(D2 . ((indx D2,D1,k) + 1)).] by A147, A193, Def5
.= [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A1, A102, Def21 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A190, A194, A195, Th5; :: thesis:
thus ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A187, A196, A197, Th10; :: thesis:

end;

suppose A198: n <> 1 ; :: thesis:

A199: (indx D2,D1,k) + 1 <= indx D2,D1,(k + 1) by A110, NAT_1:13;
consider n1 being Nat such that
A200: n = 1 + n1 by A174, NAT_1:10;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 13;
A201: (n1 + ((indx D2,D1,k) + 1)) -' 1 = ((indx D2,D1,k) + n) - 1 by A182, A200, XREAL_1:235;
A202: ( 1 <= n - 1 & n - 1 <= len MD2 )

proof

not n is trivial by A174, A198, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:31;
hence n - 1 >= 1 by XREAL_1:21; :: thesis:
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:22;
hence n - 1 <= len MD2 by A183, A185, XXREAL_0:2; :: thesis:

end;

A203: (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 ;
A204: (indx D2,D1,k) + n <> 1

proof

assume (indx D2,D1,k) + n = 1 ; :: thesis:
then indx D2,D1,k = 1 - n ;
then n + 1 <= 1 by A118, XREAL_1:21;
then n <= 1 - 1 by XREAL_1:21;
hence contradiction by A174, NAT_1:3; :: thesis:

end;

A205: lower_bound (divset MD2,n) = MD2 . (n - 1) by A187, A198, Def5
.= D2 . (((indx D2,D1,k) + n) - 1) by A108, A145, A146, A199, A200, A201, A202, JORDAN3:27 ;
A206: upper_bound (divset MD2,n) = MD2 . n by A187, A198, Def5
.= D2 . ((indx D2,D1,k) + n) by A108, A145, A146, A174, A175, A183, A185, A199, A203, JORDAN3:27 ;
then A207: divset MD2,n = [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A205, Th5;
A208: 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 A181, A204, Def5
.= [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A181, A204, Def5 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A205, A206, Th5; :: thesis:
thus ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A187, A207, A208, Th10; :: thesis:

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:

end;

then g | (divset MD2,n) = f | (divset D2,((indx D2,D1,k) + n)) by FUNCT_1:82;
hence q2 . n = (upper_volume g,MD2) . n by A188, A189, Def7, B186; :: thesis:

end;

hence q2 = upper_volume g,MD2 by A121, A173, FINSEQ_1:18; :: thesis:

end;

( len MD1 = 1 & MD1 <= MD2 )

proof

len MD1 = ((k + 1) -' (k + 1)) + 1 by A96, JORDAN3:27;
then A209: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
hence len MD1 = 1 ; :: thesis:
thus MD1 <= MD2 by A209, Th31; :: thesis:

end;

then upper_sum g,MD1 >= upper_sum g,MD2 by A151, Th32;
hence Sum q1 >= Sum q2 by A157, A171; :: thesis:

end;

A210: Sum ((upper_volume f,D1) | (k + 1)) = (Sum p1) + (Sum q1) by A120, RVSUM_1:105;
A211: Sum ((upper_volume f,D2) | (indx D2,D1,(k + 1))) = (Sum p2) + (Sum q2) by A121, RVSUM_1:105;
Sum q1 = (Sum ((upper_volume f,D1) | (k + 1))) - (Sum p1) by A210;
then Sum ((upper_volume f,D1) | (k + 1)) >= (Sum q2) + (Sum p1) by A142, XREAL_1:21;
then (Sum ((upper_volume f,D1) | (k + 1))) - (Sum q2) >= Sum p1 by XREAL_1:21;
then (Sum ((upper_volume f,D1) | (k + 1))) - (Sum q2) >= Sum p2 by A93, A101, A122, A132, 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 A211, XREAL_1:21; :: thesis:

end;

hence Sum ((upper_volume f,D1) | (k + 1)) >= Sum ((upper_volume f,D2) | (indx D2,D1,(k + 1))) ; :: thesis:

end;