let A be closed-interval Subset of REAL ; :: thesis: for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds
for i being non empty 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 empty 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 empty 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 empty 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 empty Nat st i in dom D1 holds
Sum ((upper_volume f,D1) | i) >= Sum ((upper_volume f,D2) | (indx D2,D1,i))

proof

defpred S₁[ Nat] means ( $1 in dom D1 implies Sum ((upper_volume f,D1) | $1) >= Sum ((upper_volume f,D2) | (indx D2,D1,$1)) );
A3: S₁[1]

proof

reconsider g = f | (divset D1,1) as PartFunc of (divset D1,1),REAL by PARTFUN1:43;
set B = divset D1,1;
set DD1 = mid D1,1,1;
set S1 = divs (divset D1,1);
A4: dom g = (dom f) /\ (divset D1,1) by RELAT_1:90;
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 Def5;
then A7: D2 . (indx D2,D1,1) = upper_bound (divset D1,1) by A1, A5, Def21;
D1 . 1 >= lower_bound (divset D1,1) by A6, SEQ_4:24;
then reconsider DD1 = mid D1,1,1 as Division of divset D1,1 by A5, A6, Th39;
1 in Seg (len D1) by A5, FINSEQ_1:def 3;
then A8: 1 <= len D1 by FINSEQ_1:3;
then A9: len (mid D1,1,1) = (1 -' 1) + 1 by FINSEQ_6:124;
A10: len (upper_volume g,DD1) = len DD1 by Def7
.= 1 by A9, XREAL_1:237 ;
A11: len (mid D1,1,1) = 1 by A9, XREAL_1:237;
then A12: len (mid D1,1,1) = len (D1 | 1) by A8, FINSEQ_1:80;
for k being Nat st 1 <= k & k <= len (mid D1,1,1) holds
(mid D1,1,1) . k = (D1 | 1) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (mid D1,1,1) implies (mid D1,1,1) . k = (D1 | 1) . k )
assume that
A13: 1 <= k and
A14: k <= len (mid D1,1,1) ; :: thesis: (mid D1,1,1) . k = (D1 | 1) . k
k in Seg (len (D1 | 1)) by A12, A13, A14, FINSEQ_1:3;
then k in dom (D1 | 1) by FINSEQ_1:def 3;
then k in dom (D1 | (Seg 1)) by FINSEQ_1:def 15;
then A15: (D1 | (Seg 1)) . k = D1 . k by FUNCT_1:70;
A16: k = 1 by A11, A13, A14, XXREAL_0:1;
then (mid D1,1,1) . k = D1 . ((1 + 1) - 1) by A8, FINSEQ_6:124;
hence (mid D1,1,1) . k = (D1 | 1) . k by A16, A15, FINSEQ_1:def 15; :: thesis: verum

end;

then A17: mid D1,1,1 = D1 | 1 by A12, FINSEQ_1:18;
A18: for i being Nat st 1 <= i & i <= len (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:5;
dom (D1 | (Seg 1)) = (dom D1) /\ (Seg 1) by RELAT_1:90;
then A22: 1 in dom (D1 | (Seg 1)) by A5, A21, XBOOLE_0:def 4;
dom (upper_volume f,D1) = Seg (len (upper_volume f,D1)) by FINSEQ_1:def 3
.= Seg (len D1) by Def7 ;
then A23: dom ((upper_volume f,D1) | (Seg 1)) = (Seg (len D1)) /\ (Seg 1) by RELAT_1:90
.= Seg 1 by A8, FINSEQ_1:9 ;
len DD1 = 1 by A9, XREAL_1:237;
then A24: 1 in dom DD1 by A21, FINSEQ_1:def 3;
A25: ((upper_volume f,D1) | 1) . i = ((upper_volume f,D1) | (Seg 1)) . i by FINSEQ_1:def 15
.= ((upper_volume f,D1) | (Seg 1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (upper_volume f,D1) . 1 by A23, FINSEQ_1:5, FUNCT_1:70
.= (upper_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)) by A5, Def7 ;
A26: divset D1,1 = [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by Th5
.= [.(lower_bound A),(upper_bound (divset D1,1)).] by A5, Def5
.= [.(lower_bound A),(D1 . 1).] by A5, Def5 ;
A27: (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, Def7 ;
divset DD1,1 = [.(lower_bound (divset DD1,1)),(upper_bound (divset DD1,1)).] by Th5
.= [.(lower_bound (divset D1,1)),(upper_bound (divset DD1,1)).] by A24, Def5
.= [.(lower_bound (divset D1,1)),(DD1 . 1).] by A24, Def5
.= [.(lower_bound A),((D1 | 1) . 1).] by A5, A17, Def5
.= [.(lower_bound A),((D1 | (Seg 1)) . 1).] by FINSEQ_1:def 15
.= [.(lower_bound A),(D1 . 1).] by A22, FUNCT_1:70 ;
hence (upper_volume g,DD1) . i = ((upper_volume f,D1) | 1) . i by A4, A27, A26, A25, RELAT_1:97; :: thesis: verum

end;

A28: g | (divset D1,1) is bounded_above

proof

consider a being real number such that
A29: 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,1) /\ (dom g) holds
g . x <= a

proof

let x be set ; :: thesis: ( x in (divset D1,1) /\ (dom g) implies g . x <= a )
A30: dom g c= dom f by RELAT_1:89;
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:70; :: thesis: verum

end;

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

end;

A33: rng D2 c= A by Def2;
A34: indx D2,D1,1 in dom D2 by A1, A5, Def21;
then A35: indx D2,D1,1 in Seg (len D2) by FINSEQ_1:def 3;
then A36: 1 <= indx D2,D1,1 by FINSEQ_1:3;
A37: indx D2,D1,1 <= len D2 by A35, FINSEQ_1:3;
then 1 <= len D2 by A36, XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:3;
then A38: 1 in dom D2 by FINSEQ_1:def 3;
then D2 . 1 in rng D2 by FUNCT_1:def 5;
then D2 . 1 in A by A33;
then D2 . 1 in [.(lower_bound A),(upper_bound A).] by Th5;
then D2 . 1 in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by RCOMP_1:def 1;
then ex a being Real st
( D2 . 1 = a & lower_bound A <= a & a <= upper_bound A ) ;
then D2 . 1 >= lower_bound (divset D1,1) by A5, Def5;
then reconsider DD2 = mid D2,1,(indx D2,D1,1) as Division of divset D1,1 by A34, A36, A38, A7, Th39;
indx D2,D1,1 in dom D2 by A1, A5, Def21;
then A39: indx D2,D1,1 in Seg (len D2) by FINSEQ_1:def 3;
then A40: 1 <= indx D2,D1,1 by FINSEQ_1:3;
A41: indx D2,D1,1 <= len D2 by A39, FINSEQ_1:3;
then A42: 1 <= len D2 by A40, XXREAL_0:2;
then len (mid D2,1,(indx D2,D1,1)) = ((indx D2,D1,1) -' 1) + 1 by A40, A41, FINSEQ_6:124;
then A43: len (mid D2,1,(indx D2,D1,1)) = ((indx D2,D1,1) - 1) + 1 by A40, XREAL_1:235;
then A44: len (mid D2,1,(indx D2,D1,1)) = len (D2 | (indx D2,D1,1)) by A41, FINSEQ_1:80;
A45: for k being Nat st 1 <= k & k <= len (mid D2,1,(indx D2,D1,1)) holds
(mid D2,1,(indx D2,D1,1)) . k = (D2 | (indx D2,D1,1)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (mid D2,1,(indx D2,D1,1)) implies (mid D2,1,(indx D2,D1,1)) . k = (D2 | (indx D2,D1,1)) . k )
assume that
A46: 1 <= k and
A47: k <= len (mid D2,1,(indx D2,D1,1)) ; :: thesis: (mid D2,1,(indx D2,D1,1)) . k = (D2 | (indx D2,D1,1)) . k
k in Seg (len (D2 | (indx D2,D1,1))) by A44, A46, A47, FINSEQ_1:3;
then k in dom (D2 | (indx D2,D1,1)) by FINSEQ_1:def 3;
then k in dom (D2 | (Seg (indx D2,D1,1))) by FINSEQ_1:def 15;
then A48: (D2 | (Seg (indx D2,D1,1))) . k = D2 . k by FUNCT_1:70;
k in NAT by ORDINAL1:def 13;
then (mid D2,1,(indx D2,D1,1)) . k = D2 . ((k + 1) -' 1) by A40, A41, A42, A46, A47, FINSEQ_6:124;
then (mid D2,1,(indx D2,D1,1)) . k = D2 . ((k + 1) - 1) by NAT_1:11, XREAL_1:235;
hence (mid D2,1,(indx D2,D1,1)) . k = (D2 | (indx D2,D1,1)) . k by A48, FINSEQ_1:def 15; :: thesis: verum

end;

then A49: mid D2,1,(indx D2,D1,1) = D2 | (indx D2,D1,1) by A44, FINSEQ_1:18;
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, Def7;
then A54: i in Seg (len DD2) by A51, FINSEQ_1:3;
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:7;
then i in Seg (len D2) by A43, A54;
then A56: i in dom D2 by FINSEQ_1:def 3;

now

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 15;
then 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by RELAT_1:90;
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, Th5
.= [.(lower_bound A),(upper_bound (divset D2,1)).] by A59, Def5
.= [.(lower_bound A),(D2 . 1).] by A59, Def5 ;
divset DD2,i = [.(lower_bound (divset DD2,1)),(upper_bound (divset DD2,1)).] by A57, Th5
.= [.(lower_bound (divset D1,1)),(upper_bound (divset DD2,1)).] by A55, A57, Def5
.= [.(lower_bound (divset D1,1)),(DD2 . 1).] by A55, A57, Def5
.= [.(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 15
.= [.(lower_bound (divset D1,1)),(D2 . 1).] by A58, FUNCT_1:70
.= [.(lower_bound A),(D2 . 1).] by A5, Def5 ;
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)))

proof

not i is trivial by A51, A61, NAT_2:def 1;
then A63: i >= 1 + 1 by NAT_2:31;
then A64: 1 <= i - 1 by XREAL_1:21;
A65: ex j being Nat st i = 1 + j by A51, NAT_1:10;
A66: i - 1 <= (indx D2,D1,1) - 0 by A43, A53, XREAL_1:15;
then i - 1 <= len D2 by A37, XXREAL_0:2;
then i - 1 in Seg (len D2) by A65, A64, FINSEQ_1:3;
then A67: i - 1 in dom D2 by FINSEQ_1:def 3;
i - 1 >= 1 by A63, XREAL_1:21;
then i - 1 in Seg (indx D2,D1,1) by A65, A66, FINSEQ_1:3;
then i - 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by A67, XBOOLE_0:def 4;
hence i - 1 in dom (D2 | (Seg (indx D2,D1,1))) by RELAT_1:90; :: thesis: verum

end;

DD2 . (i - 1) = (D2 | (indx D2,D1,1)) . (i - 1) by A44, A45, FINSEQ_1:18
.= (D2 | (Seg (indx D2,D1,1))) . (i - 1) by FINSEQ_1:def 15 ;
then A68: DD2 . (i - 1) = D2 . (i - 1) by A62, FUNCT_1:70;
i <= len D2 by A43, A37, A53, XXREAL_0:2;
then i in Seg (len D2) by A51, FINSEQ_1:3;
then i in dom D2 by FINSEQ_1:def 3;
then i in (dom D2) /\ (Seg (indx D2,D1,1)) by A43, A54, XBOOLE_0:def 4;
then A69: i in dom (D2 | (Seg (indx D2,D1,1))) by RELAT_1:90;
DD2 . i = (D2 | (indx D2,D1,1)) . i by A44, A45, FINSEQ_1:18
.= (D2 | (Seg (indx D2,D1,1))) . i by FINSEQ_1:def 15 ;
then A70: DD2 . i = D2 . i by A69, FUNCT_1:70;
A71: divset D2,i = [.(lower_bound (divset D2,i)),(upper_bound (divset D2,i)).] by Th5
.= [.(D2 . (i - 1)),(upper_bound (divset D2,i)).] by A56, A61, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A56, A61, Def5 ;
divset DD2,i = [.(lower_bound (divset DD2,i)),(upper_bound (divset DD2,i)).] by Th5
.= [.(DD2 . (i - 1)),(upper_bound (divset DD2,i)).] by A55, A61, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A55, A61, A68, A70, Def5 ;
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, Def7;
Seg (indx D2,D1,1) c= Seg (len D2) by A41, FINSEQ_1:7;
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

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 15;
then 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by RELAT_1:90;
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:154;
lower_bound (divset D2,i) = lower_bound A by A76, A77, Def5;
then A79: lower_bound (divset D2,i) = lower_bound (divset D1,1) by A5, Def5;
upper_bound (divset D2,i) = D2 . 1 by A76, A77, Def5;
then upper_bound (divset D2,i) <= D1 . 1 by A1, A5, A78, Def21;
then A80: upper_bound (divset D2,i) <= upper_bound (divset D1,1) by A5, Def5;
lower_bound (divset D1,1) <= upper_bound (divset D1,1) by Th4;
hence lower_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by 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 Th4;
then upper_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by 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:31;
then A82: 1 <= i - 1 by XREAL_1:21;
A83: ex j being Nat st i = 1 + j by A51, NAT_1:10;
A84: rng D2 c= A by Def2;
A85: lower_bound (divset D2,i) = D2 . (i - 1) by A73, A81, Def5;
A86: lower_bound (divset D1,1) = lower_bound A by A5, Def5;
A87: i - 1 <= (indx D2,D1,1) - 0 by A43, A53, XREAL_1:15;
then i - 1 <= len D2 by A37, XXREAL_0:2;
then i - 1 in Seg (len D2) by A83, A82, FINSEQ_1:3;
then A88: i - 1 in dom D2 by FINSEQ_1:def 3;
then D2 . (i - 1) in rng D2 by FUNCT_1:def 5;
then A89: lower_bound (divset D2,i) >= lower_bound (divset D1,1) by A85, A86, A84, SEQ_4:def 5;
A90: upper_bound (divset D1,1) = D1 . 1 by A5, Def5;
D2 . (i - 1) <= D2 . (indx D2,D1,1) by A34, A87, A88, SEQ_4:154;
then lower_bound (divset D2,i) <= upper_bound (divset D1,1) by A1, A5, A85, A90, Def21;
then lower_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by 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, Def5;
D2 . i in rng D2 by A73, FUNCT_1:def 5;
then A92: upper_bound (divset D2,i) >= lower_bound (divset D1,1) by A91, A86, A84, SEQ_4:def 5;
D2 . i <= D2 . (indx D2,D1,1) by A43, A34, A53, A73, SEQ_4:154;
then upper_bound (divset D2,i) <= upper_bound (divset D1,1) by A1, A5, A91, A90, Def21;
then upper_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by 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 Th5;
A94: Seg (indx D2,D1,1) c= Seg (len D2) by A41, FINSEQ_1:7;
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 Th5;
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:90
.= (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 Def7
.= 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 15
.= (upper_volume f,D2) . i by A43, A54, A97, FUNCT_1:70
.= (upper_bound (rng (f | (divset D2,i)))) * (vol (divset D2,i)) by A95, Def7 ;
hence (upper_volume g,DD2) . i = ((upper_volume f,D2) | (indx D2,D1,1)) . i by A72, A96, FUNCT_1:82; :: thesis: verum

end;

1 <= len (upper_volume f,D1) by A8, Def7;
then len (upper_volume g,DD1) = len ((upper_volume f,D1) | 1) by A10, FINSEQ_1:80;
then A98: upper_volume g,DD1 = (upper_volume f,D1) | 1 by A18, FINSEQ_1:18;
A99: indx D2,D1,1 <= len (upper_volume f,D2) by A41, Def7;
len (upper_volume g,DD2) = indx D2,D1,1 by A43, Def7;
then A100: len (upper_volume g,DD2) = len ((upper_volume f,D2) | (indx D2,D1,1)) by A99, FINSEQ_1:80;
dom g = A /\ (divset D1,1) by A4, FUNCT_2:def 1;
then dom g = divset D1,1 by A5, Th10, XBOOLE_1:28;
then g is total by PARTFUN1:def 4;
then upper_sum g,DD1 >= upper_sum g,DD2 by A11, A28, Th32;
hence Sum ((upper_volume f,D1) | 1) >= Sum ((upper_volume f,D2) | (indx D2,D1,1)) by A98, A100, A50, FINSEQ_1:18; :: thesis: verum

end;

A101: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[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: S₁[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:3;
A106: k + 1 <= len D1 by A104, FINSEQ_1:3;

now

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, Def7;
then A109: len ((upper_volume f,D1) | (k + 1)) = k + 1 by FINSEQ_1:80;
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:26;
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 Def7;
then A116: len p1 = len ((upper_volume f,D1) | k) by A110, 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: ( 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:3;
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 15;
k <= k + 1 by NAT_1:11;
then A122: Seg k c= Seg (k + 1) by FINSEQ_1:7;
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:80 ;
dom ((upper_volume f,D1) | k) = Seg (len ((upper_volume f,D1) | k)) by FINSEQ_1:def 3
.= Seg k by A115, FINSEQ_1:80 ;
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 15;
A125: ((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 A124, FUNCT_1:70 ;
A126: ((upper_volume f,D1) | k) . i = ((upper_volume f,D1) | (Seg k)) . i by FINSEQ_1:def 15
.= (upper_volume f,D1) . i by A121, FUNCT_1:70 ;
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:18;
A128: indx D2,D1,(k + 1) in dom D2 by A1, A103, Def21;
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:3;
not k + 1 is trivial by A107, NAT_2:def 1;
then k + 1 >= 2 by NAT_2:31;
then k >= (1 + 1) - 1 by XREAL_1:22;
then A131: k in Seg (len D1) by A114, FINSEQ_1:3;
then A132: k in dom D1 by FINSEQ_1:def 3;
then A133: indx D2,D1,k in dom D2 by A1, Def21;
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:154;
D1 . k = D2 . (indx D2,D1,k) by A1, A132, Def21;
hence contradiction by A1, A103, A136, A135, Def21; :: 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, Def21;
then D1 . (k + 1) < D1 . k by A1, A132, A138, Def21;
hence contradiction by A103, A132, NAT_1:11, SEQ_4:154; :: 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 13;
A140: len (upper_volume f,D2) = len D2 by Def7;
then A141: indx D2,D1,(k + 1) <= len (upper_volume f,D2) by A129, FINSEQ_1:3;
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:80;
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:26;
indx D2,D1,k in dom D2 by A1, A132, Def21;
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:3;
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:105;
A148: indx D2,D1,k <= len (upper_volume f,D2) by A145, FINSEQ_1:3;
then A149: len p2 = len ((upper_volume f,D2) | (indx D2,D1,k)) by A142, 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: ( 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:3;
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 15;
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:80 ;
A156: Seg (indx D2,D1,k) c= Seg (indx D2,D1,(k + 1)) by A137, FINSEQ_1:7;
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:80 ;
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 15;
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 15
.= (upper_volume f,D2) . i by A157, FUNCT_1:70 ;
A159: ((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 A154, FUNCT_1:70 ;
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:18;
A161: indx D2,D1,(k + 1) <= len D2 by A129, FINSEQ_1:3;
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));
set S1 = divs (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:43;
(k + 1) - 1 = k ;
then A165: lower_bound (divset D1,(k + 1)) = D1 . k by A103, A107, Def5;
D2 . (indx D2,D1,(k + 1)) = D1 . (k + 1) by A1, A103, Def21;
then A166: D2 . (indx D2,D1,(k + 1)) = upper_bound (divset D1,(k + 1)) by A103, A107, Def5;
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:3;
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:154;
then D2 . ((indx D2,D1,k) + 1) >= lower_bound (divset D1,(k + 1)) by A1, A132, A165, Def21;
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, Th39;
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:235
.= (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:80 ;
then A173: dom ((upper_volume f,D2) | (indx D2,D1,(k + 1))) c= Seg (len D2) by A161, FINSEQ_1:7;
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:124;
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
A178: n in Seg (len q2) by A176, A177, FINSEQ_1:3;
then A179: n in dom q2 by FINSEQ_1:def 3;
then A180: (indx D2,D1,k) + n in dom ((upper_volume f,D2) | (indx D2,D1,(k + 1))) by A142, A144, FINSEQ_1:41;
then A181: (indx D2,D1,k) + n in dom ((upper_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
A182: q2 . n = ((upper_volume f,D2) | (indx D2,D1,(k + 1))) . ((indx D2,D1,k) + n) by A142, A144, A179, 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 A181, FUNCT_1:70
.= (upper_bound (rng (f | (divset D2,((indx D2,D1,k) + n))))) * (vol (divset D2,((indx D2,D1,k) + n))) by A180, A174, Def7 ;
(indx D2,D1,k) + n in Seg (len D2) by A180, A173;
then A183: (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, A180, FINSEQ_1:3;
then A184: n <= ID by A162, XREAL_1:21;
then n in Seg ID by A176, FINSEQ_1:3;
then A185: 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, A184, A175, FINSEQ_1:3;
then A186: n in dom (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) by FINSEQ_1:def 3;
A187: 1 <= (indx D2,D1,k) + n by A172, A180, FINSEQ_1:3;
A188: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )

proof

now

per cases ( n = 1 or n <> 1 ) ;

suppose A189: 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 A190: (indx D2,D1,k) + 1 <= len D2 by A180, A173, FINSEQ_1:3;
A191: 1 <= (indx D2,D1,k) + 1 by A172, A180, A189, FINSEQ_1:3;
A192: upper_bound (divset MD2,1) = (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) . 1 by A185, A189, Def5
.= D2 . (1 + (indx D2,D1,k)) by A130, A161, A191, A190, FINSEQ_6:124 ;
A193: (indx D2,D1,k) + 1 <> 1 by A146, NAT_1:13;
A194: (k + 1) - 1 = k ;
A195: lower_bound (divset MD2,1) = lower_bound (divset D1,(k + 1)) by A185, A189, Def5
.= D1 . k by A103, A107, A194, Def5 ;
A196: 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 A189, Th5
.= [.(D2 . (((indx D2,D1,k) + 1) - 1)),(upper_bound (divset D2,((indx D2,D1,k) + 1))).] by A169, A193, Def5
.= [.(D2 . (indx D2,D1,k)),(D2 . ((indx D2,D1,k) + 1)).] by A169, A193, Def5
.= [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A1, A132, Def21 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A189, A195, A192, Th5; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )
divset MD2,n = [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A189, A195, A192, Th5;
hence ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A185, A196, Th10; :: thesis: verum

end;

suppose A197: 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) )

A198: (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:21;
then n <= 1 - 1 by XREAL_1:21;
hence contradiction by A176, NAT_1:3; :: thesis: verum

end;

A199: 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 A183, A198, Def5
.= [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A183, A198, Def5 ;
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:22;
then A200: n - 1 <= len MD2 by A184, A175, XXREAL_0:2;
consider n1 being Nat such that
A201: n = 1 + n1 by A176, NAT_1:10;
not n is trivial by A176, A197, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:31;
then A202: 1 <= n - 1 by XREAL_1:21;
A203: (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 13;
A204: (n1 + ((indx D2,D1,k) + 1)) -' 1 = ((indx D2,D1,k) + n) - 1 by A187, A201, XREAL_1:235;
A205: (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 ;
A206: lower_bound (divset MD2,n) = MD2 . (n - 1) by A185, A197, Def5
.= D2 . (((indx D2,D1,k) + n) - 1) by A130, A161, A168, A164, A203, A201, A204, A202, A200, FINSEQ_6:124 ;
A207: upper_bound (divset MD2,n) = MD2 . n by A185, A197, Def5
.= D2 . ((indx D2,D1,k) + n) by A130, A161, A168, A164, A176, A178, A184, A175, A203, A205, FINSEQ_6:124 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A206, A199, Th5; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )
divset MD2,n = [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A206, A207, Th5;
hence ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A185, A199, Th10; :: thesis: verum

end;

end;

end;

hence ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) ; :: thesis: verum

end;

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

end;

(k + 1) - 1 = k ;
then A208: lower_bound (divset D1,(k + 1)) = D1 . k by A103, A107, Def5;
D1 . (k + 1) = upper_bound (divset D1,(k + 1)) by A103, A107, Def5;
then reconsider MD1 = mid D1,(k + 1),(k + 1) as Division of divset D1,(k + 1) by A103, A113, A132, A208, Th39, SEQ_4:154;
A209: g | (divset D1,(k + 1)) is bounded_above

proof

consider a being real number such that
A210: 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: ( x in (divset D1,(k + 1)) /\ (dom g) implies g . x <= a )
A211: dom g c= dom f by RELAT_1:89;
assume x in (divset D1,(k + 1)) /\ (dom g) ; :: thesis: g . x <= a
then A212: x in dom g by XBOOLE_0:def 4;
A213: A /\ (dom f) = dom f by XBOOLE_1:28;
then x in A /\ (dom f) by A212, A211;
then reconsider x = x as Element of A ;
f . x <= a by A210, A212, A213, A211;
hence g . x <= a by A212, FUNCT_1:70; :: thesis: verum

end;

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

end;

len MD1 = ((k + 1) -' (k + 1)) + 1 by A105, A106, FINSEQ_6:124;
then A214: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
then A215: dom q1 = dom MD1 by A111, FINSEQ_3:31;
A216: 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:6;
then k + 1 in dom ((upper_volume f,D1) | (k + 1)) by FINSEQ_1:def 3;
then A217: k + 1 in dom ((upper_volume f,D1) | (Seg (k + 1))) by FINSEQ_1:def 15;
A218: MD1 . 1 = D1 . (k + 1) by A105, A106, FINSEQ_6:124;
1 in Seg (len MD1) by A214, FINSEQ_1:5;
then A219: 1 in dom MD1 by FINSEQ_1:def 3;
divset MD1,1 = [.(lower_bound (divset MD1,1)),(upper_bound (divset MD1,1)).] by Th5;
then A220: divset MD1,1 = [.(lower_bound (divset D1,(k + 1))),(upper_bound (divset MD1,1)).] by A219, Def5
.= [.(lower_bound (divset D1,(k + 1))),(D1 . (k + 1)).] by A219, A218, Def5 ;
(k + 1) - 1 = k ;
then A221: lower_bound (divset D1,(k + 1)) = D1 . k by A103, A107, Def5;
let n be Nat; :: thesis: ( 1 <= n & n <= len q1 implies q1 . n = (upper_volume g,MD1) . n )
assume that
A222: 1 <= n and
A223: n <= len q1 ; :: thesis: q1 . n = (upper_volume g,MD1) . n
A224: n = 1 by A111, A222, A223, XXREAL_0:1;
n in Seg (len q1) by A222, A223, FINSEQ_1:3;
then A225: n in dom q1 by FINSEQ_1:def 3;
upper_bound (divset D1,(k + 1)) = D1 . (k + 1) by A103, A107, Def5;
then divset D1,(k + 1) = [.(D1 . k),(D1 . (k + 1)).] by A221, Th5;
then A226: (upper_volume g,MD1) . n = (upper_bound (rng (g | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by A215, A224, A225, A220, A221, Def7;
((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 A217, FUNCT_1:70 ;
then q1 . n = (upper_volume f,D1) . (k + 1) by A110, A112, A224, A225, FINSEQ_1:def 7
.= (upper_bound (rng (f | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by A103, Def7 ;
hence q1 . n = (upper_volume g,MD1) . n by A226, FUNCT_1:82; :: thesis: verum

end;

len q1 = len (upper_volume g,MD1) by A111, A214, Def7;
then A227: q1 = upper_volume g,MD1 by A216, FINSEQ_1:18;
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 A103, Th10, XBOOLE_1:28;
then A228: g is total by PARTFUN1:def 4;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A105, A106, FINSEQ_6:124;
then len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
then A229: upper_sum g,MD1 >= upper_sum g,MD2 by A209, A228, Th32;
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 A130, A161, A167, A168, A164, A170, FINSEQ_6:124 ;
hence Sum q1 >= Sum q2 by A143, A227, A171, A229, FINSEQ_1:18; :: thesis: verum

end;

Sum ((upper_volume f,D1) | (k + 1)) = (Sum p1) + (Sum q1) by A112, RVSUM_1:105;
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: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 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:21; :: 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 empty Nat holds S₁[k] from NAT_1:sch 10(A3, A101); :: thesis: verum

end;

hence for i being non empty 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