let A be closed-interval Subset of REAL ; :: thesis: for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds
for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i))
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st D1 <= D2 & f | A is bounded_below holds
for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i))
let f be Function of A,REAL ; :: thesis: ( D1 <= D2 & f | A is bounded_below implies for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i)) )
assume that
A1: D1 <= D2 and
A2: f | A is bounded_below ; :: thesis: for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i))
for i being non empty Nat st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i))

proof

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

proof

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

proof

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

end;

then A17: mid D1,1,1 = D1 | 1 by A12, FINSEQ_1:18;
A18: for i being Nat st 1 <= i & i <= len (lower_volume g,DD1) holds
(lower_volume g,DD1) . i = ((lower_volume f,D1) | 1) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume g,DD1) implies (lower_volume g,DD1) . i = ((lower_volume f,D1) | 1) . i )
assume that
A19: 1 <= i and
A20: i <= len (lower_volume g,DD1) ; :: thesis: (lower_volume g,DD1) . i = ((lower_volume f,D1) | 1) . i
A21: 1 in Seg 1 by FINSEQ_1:5;
dom (D1 | (Seg 1)) = (dom D1) /\ (Seg 1) by RELAT_1:90;
then A22: 1 in dom (D1 | (Seg 1)) by A5, A21, XBOOLE_0:def 4;
dom (lower_volume f,D1) = Seg (len (lower_volume f,D1)) by FINSEQ_1:def 3
.= Seg (len D1) by Def8 ;
then A23: dom ((lower_volume f,D1) | (Seg 1)) = (Seg (len D1)) /\ (Seg 1) by RELAT_1:90
.= Seg 1 by A8, FINSEQ_1:9 ;
len DD1 = 1 by A9, XREAL_1:237;
then A24: 1 in dom DD1 by A21, FINSEQ_1:def 3;
A25: ((lower_volume f,D1) | 1) . i = ((lower_volume f,D1) | (Seg 1)) . i by FINSEQ_1:def 15
.= ((lower_volume f,D1) | (Seg 1)) . 1 by A10, A19, A20, XXREAL_0:1
.= (lower_volume f,D1) . 1 by A23, FINSEQ_1:5, FUNCT_1:70
.= (lower_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)) by A5, Def8 ;
A26: divset D1,1 = [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by Th5
.= [.(lower_bound A),(upper_bound (divset D1,1)).] by A5, Def5
.= [.(lower_bound A),(D1 . 1).] by A5, Def5 ;
A27: (lower_volume g,DD1) . i = (lower_volume g,DD1) . 1 by A10, A19, A20, XXREAL_0:1
.= (lower_bound (rng (g | (divset DD1,1)))) * (vol (divset DD1,1)) by A24, Def8 ;
divset DD1,1 = [.(lower_bound (divset DD1,1)),(upper_bound (divset DD1,1)).] by Th5
.= [.(lower_bound (divset D1,1)),(upper_bound (divset DD1,1)).] by A24, Def5
.= [.(lower_bound (divset D1,1)),(DD1 . 1).] by A24, Def5
.= [.(lower_bound A),((D1 | 1) . 1).] by A5, A17, Def5
.= [.(lower_bound A),((D1 | (Seg 1)) . 1).] by FINSEQ_1:def 15
.= [.(lower_bound A),(D1 . 1).] by A22, FUNCT_1:70 ;
hence (lower_volume g,DD1) . i = ((lower_volume f,D1) | 1) . i by A4, A27, A26, A25, RELAT_1:97; :: thesis: verum

end;

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

proof

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

proof

let x be set ; :: thesis: ( x in (divset D1,1) /\ (dom g) implies a <= g . x )
A30: dom g c= dom f by RELAT_1:89;
assume x in (divset D1,1) /\ (dom g) ; :: thesis: a <= g . x
then A31: x in dom g by XBOOLE_0:def 4;
A32: A /\ (dom f) = dom f by XBOOLE_1:28;
then reconsider x = x as Element of A by A31, A30, XBOOLE_0:def 4;
a <= f . x by A29, A31, A32, A30;
hence a <= g . x by A31, FUNCT_1:70; :: thesis: verum

end;

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

end;

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

proof

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

end;

then A50: mid D2,1,(indx D2,D1,1) = D2 | (indx D2,D1,1) by A44, FINSEQ_1:18;
A51: for i being Nat st 1 <= i & i <= len (lower_volume g,DD2) holds
(lower_volume g,DD2) . i = ((lower_volume f,D2) | (indx D2,D1,1)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (lower_volume g,DD2) implies (lower_volume g,DD2) . i = ((lower_volume f,D2) | (indx D2,D1,1)) . i )
assume that
A52: 1 <= i and
A53: i <= len (lower_volume g,DD2) ; :: thesis: (lower_volume g,DD2) . i = ((lower_volume f,D2) | (indx D2,D1,1)) . i
A54: i <= len DD2 by A53, Def8;
then A55: i in Seg (len DD2) by A52, FINSEQ_1:3;
then A56: i in dom DD2 by FINSEQ_1:def 3;
divset DD2,i = divset D2,i

proof

Seg (indx D2,D1,1) c= Seg (len D2) by A41, FINSEQ_1:7;
then i in Seg (len D2) by A43, A55;
then A57: i in dom D2 by FINSEQ_1:def 3;

now

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

suppose A58: i = 1 ; :: thesis: divset DD2,i = divset D2,i

then A59: 1 in dom (D2 | (Seg (indx D2,D1,1))) by A50, A56, FINSEQ_1:def 15;
then 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by RELAT_1:90;
then A60: 1 in dom D2 by XBOOLE_0:def 4;
A61: divset D2,i = [.(lower_bound (divset D2,1)),(upper_bound (divset D2,1)).] by A58, Th5
.= [.(lower_bound A),(upper_bound (divset D2,1)).] by A60, Def5
.= [.(lower_bound A),(D2 . 1).] by A60, Def5 ;
divset DD2,i = [.(lower_bound (divset DD2,1)),(upper_bound (divset DD2,1)).] by A58, Th5
.= [.(lower_bound (divset D1,1)),(upper_bound (divset DD2,1)).] by A56, A58, Def5
.= [.(lower_bound (divset D1,1)),(DD2 . 1).] by A56, A58, Def5
.= [.(lower_bound (divset D1,1)),((D2 | (indx D2,D1,1)) . 1).] by A45, A54, A58
.= [.(lower_bound (divset D1,1)),((D2 | (Seg (indx D2,D1,1))) . 1).] by FINSEQ_1:def 15
.= [.(lower_bound (divset D1,1)),(D2 . 1).] by A59, FUNCT_1:70
.= [.(lower_bound A),(D2 . 1).] by A5, Def5 ;
hence divset DD2,i = divset D2,i by A61; :: thesis: verum

end;

suppose A62: i <> 1 ; :: thesis: divset DD2,i = divset D2,i

A63: i - 1 in dom (D2 | (Seg (indx D2,D1,1)))

proof

not i is trivial by A52, A62, NAT_2:def 1;
then A64: i >= 1 + 1 by NAT_2:31;
then A65: 1 <= i - 1 by XREAL_1:21;
A66: ex j being Nat st i = 1 + j by A52, NAT_1:10;
A67: i - 1 <= (indx D2,D1,1) - 0 by A43, A54, XREAL_1:15;
then i - 1 <= len D2 by A37, XXREAL_0:2;
then i - 1 in Seg (len D2) by A66, A65, FINSEQ_1:3;
then A68: i - 1 in dom D2 by FINSEQ_1:def 3;
i - 1 >= 1 by A64, XREAL_1:21;
then i - 1 in Seg (indx D2,D1,1) by A66, A67, FINSEQ_1:3;
then i - 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by A68, 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 A69: DD2 . (i - 1) = D2 . (i - 1) by A63, FUNCT_1:70;
i <= len D2 by A43, A37, A54, XXREAL_0:2;
then i in Seg (len D2) by A52, FINSEQ_1:3;
then i in dom D2 by FINSEQ_1:def 3;
then i in (dom D2) /\ (Seg (indx D2,D1,1)) by A43, A55, XBOOLE_0:def 4;
then A70: i in dom (D2 | (Seg (indx D2,D1,1))) by RELAT_1:90;
DD2 . i = (D2 | (indx D2,D1,1)) . i by A44, A45, FINSEQ_1:18
.= (D2 | (Seg (indx D2,D1,1))) . i by FINSEQ_1:def 15 ;
then A71: DD2 . i = D2 . i by A70, FUNCT_1:70;
A72: divset D2,i = [.(lower_bound (divset D2,i)),(upper_bound (divset D2,i)).] by Th5
.= [.(D2 . (i - 1)),(upper_bound (divset D2,i)).] by A57, A62, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A57, A62, Def5 ;
divset DD2,i = [.(lower_bound (divset DD2,i)),(upper_bound (divset DD2,i)).] by Th5
.= [.(DD2 . (i - 1)),(upper_bound (divset DD2,i)).] by A56, A62, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A56, A62, A69, A71, Def5 ;
hence divset DD2,i = divset D2,i by A72; :: thesis: verum

end;

end;

end;

hence divset DD2,i = divset D2,i ; :: thesis: verum

end;

then A73: (lower_volume g,DD2) . i = (lower_bound (rng (g | (divset D2,i)))) * (vol (divset D2,i)) by A56, Def8;
Seg (indx D2,D1,1) c= Seg (len D2) by A41, FINSEQ_1:7;
then i in Seg (len D2) by A43, A55;
then A74: i in dom D2 by FINSEQ_1:def 3;
A75: i in dom DD2 by A55, FINSEQ_1:def 3;

A76: now

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

suppose A77: i = 1 ; :: thesis: ( lower_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] & upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] )

then 1 in dom (D2 | (Seg (indx D2,D1,1))) by A50, A75, FINSEQ_1:def 15;
then 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by RELAT_1:90;
then A78: 1 in dom D2 by XBOOLE_0:def 4;
then D2 . 1 <= D2 . (indx D2,D1,1) by A34, A36, SEQ_4:154;
then A79: D2 . 1 <= D1 . 1 by A1, A5, Def21;
lower_bound (divset D2,i) = lower_bound A by A77, A78, Def5;
then A80: lower_bound (divset D2,i) = lower_bound (divset D1,1) by A5, Def5;
upper_bound (divset D2,i) = D2 . 1 by A77, A78, Def5;
then A81: upper_bound (divset D2,i) <= upper_bound (divset D1,1) by A5, A79, Def5;
lower_bound (divset D1,1) <= upper_bound (divset D1,1) by Th4;
hence lower_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by A80, XXREAL_1:1; :: thesis: upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).]
lower_bound (divset D2,i) <= upper_bound (divset D2,i) by Th4;
then upper_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by A80, A81;
hence upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by RCOMP_1:def 1; :: thesis: verum

end;

suppose A82: i <> 1 ; :: thesis: ( lower_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] & upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] )

then not i is trivial by A52, NAT_2:def 1;
then i >= 1 + 1 by NAT_2:31;
then A83: 1 <= i - 1 by XREAL_1:21;
A84: ex j being Nat st i = 1 + j by A52, NAT_1:10;
A85: rng D2 c= A by Def2;
A86: lower_bound (divset D2,i) = D2 . (i - 1) by A74, A82, Def5;
A87: lower_bound (divset D1,1) = lower_bound A by A5, Def5;
A88: i - 1 <= (indx D2,D1,1) - 0 by A43, A54, XREAL_1:15;
then i - 1 <= len D2 by A37, XXREAL_0:2;
then i - 1 in Seg (len D2) by A84, A83, FINSEQ_1:3;
then A89: i - 1 in dom D2 by FINSEQ_1:def 3;
then D2 . (i - 1) in rng D2 by FUNCT_1:def 5;
then A90: lower_bound (divset D2,i) >= lower_bound (divset D1,1) by A86, A87, A85, SEQ_4:def 5;
A91: upper_bound (divset D1,1) = D1 . 1 by A5, Def5;
D2 . (i - 1) <= D2 . (indx D2,D1,1) by A34, A88, A89, SEQ_4:154;
then lower_bound (divset D2,i) <= upper_bound (divset D1,1) by A1, A5, A86, A91, Def21;
then lower_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by A90;
hence lower_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by RCOMP_1:def 1; :: thesis: upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).]
A92: upper_bound (divset D2,i) = D2 . i by A74, A82, Def5;
D2 . i in rng D2 by A74, FUNCT_1:def 5;
then A93: upper_bound (divset D2,i) >= lower_bound (divset D1,1) by A92, A87, A85, SEQ_4:def 5;
D2 . i <= D2 . (indx D2,D1,1) by A43, A34, A54, A74, SEQ_4:154;
then upper_bound (divset D2,i) <= upper_bound (divset D1,1) by A1, A5, A92, A91, Def21;
then upper_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by A93;
hence upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by RCOMP_1:def 1; :: thesis: verum

end;

end;

end;

A94: divset D1,1 = [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by Th5;
A95: Seg (indx D2,D1,1) c= Seg (len D2) by A41, FINSEQ_1:7;
then i in Seg (len D2) by A43, A55;
then A96: i in dom D2 by FINSEQ_1:def 3;
divset D2,i = [.(lower_bound (divset D2,i)),(upper_bound (divset D2,i)).] by Th5;
then A97: divset D2,i c= divset D1,1 by A94, A76, XXREAL_2:def 12;
A98: dom ((lower_volume f,D2) | (Seg (indx D2,D1,1))) = (dom (lower_volume f,D2)) /\ (Seg (indx D2,D1,1)) by RELAT_1:90
.= (Seg (len (lower_volume f,D2))) /\ (Seg (indx D2,D1,1)) by FINSEQ_1:def 3
.= (Seg (len D2)) /\ (Seg (indx D2,D1,1)) by Def8
.= Seg (indx D2,D1,1) by A95, XBOOLE_1:28 ;
((lower_volume f,D2) | (indx D2,D1,1)) . i = ((lower_volume f,D2) | (Seg (indx D2,D1,1))) . i by FINSEQ_1:def 15
.= (lower_volume f,D2) . i by A43, A55, A98, FUNCT_1:70
.= (lower_bound (rng (f | (divset D2,i)))) * (vol (divset D2,i)) by A96, Def8 ;
hence (lower_volume g,DD2) . i = ((lower_volume f,D2) | (indx D2,D1,1)) . i by A73, A97, FUNCT_1:82; :: thesis: verum

end;

1 <= len (lower_volume f,D1) by A8, Def8;
then len (lower_volume g,DD1) = len ((lower_volume f,D1) | 1) by A10, FINSEQ_1:80;
then A99: lower_volume g,DD1 = (lower_volume f,D1) | 1 by A18, FINSEQ_1:18;
A100: indx D2,D1,1 <= len (lower_volume f,D2) by A41, Def8;
len (lower_volume g,DD2) = indx D2,D1,1 by A43, Def8;
then A101: len (lower_volume g,DD2) = len ((lower_volume f,D2) | (indx D2,D1,1)) by A100, FINSEQ_1:80;
dom g = A /\ (divset D1,1) by A4, FUNCT_2:def 1;
then dom g = divset D1,1 by A5, Th10, XBOOLE_1:28;
then g is total by PARTFUN1:def 4;
then lower_sum g,DD1 <= lower_sum g,DD2 by A11, A28, Th33;
hence Sum ((lower_volume f,D1) | 1) <= Sum ((lower_volume f,D2) | (indx D2,D1,1)) by A99, A101, A51, FINSEQ_1:18; :: thesis: verum

end;

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

proof

let k be non empty Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A103: ( k in dom D1 implies Sum ((lower_volume f,D1) | k) <= Sum ((lower_volume f,D2) | (indx D2,D1,k)) ) ; :: thesis: S₁[k + 1]
assume A104: k + 1 in dom D1 ; :: thesis: Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1)))
then A105: k + 1 in Seg (len D1) by FINSEQ_1:def 3;
then A106: 1 <= k + 1 by FINSEQ_1:3;
A107: k + 1 <= len D1 by A105, FINSEQ_1:3;

now

per cases ( 1 = k + 1 or 1 <> k + 1 ) ;

suppose 1 = k + 1 ; :: thesis: Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1)))

hence Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1))) by A3, A104; :: thesis: verum

end;

suppose A108: 1 <> k + 1 ; :: thesis: Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1)))

set IDK = indx D2,D1,k;
set IDK1 = indx D2,D1,(k + 1);
set K1D2 = (lower_volume f,D2) | (indx D2,D1,(k + 1));
set KD1 = (lower_volume f,D1) | k;
set K1D1 = (lower_volume f,D1) | (k + 1);
set n = k + 1;
A109: k + 1 <= len (lower_volume f,D1) by A107, Def8;
then A110: len ((lower_volume f,D1) | (k + 1)) = k + 1 by FINSEQ_1:80;
then consider p1, q1 being FinSequence of REAL such that
A111: len p1 = k and
A112: len q1 = 1 and
A113: (lower_volume f,D1) | (k + 1) = p1 ^ q1 by FINSEQ_2:26;
A114: k <= k + 1 by NAT_1:11;
then A115: k <= len D1 by A107, XXREAL_0:2;
then A116: k <= len (lower_volume f,D1) by Def8;
then A117: len p1 = len ((lower_volume f,D1) | k) by A111, FINSEQ_1:80;
for i being Nat st 1 <= i & i <= len p1 holds
p1 . i = ((lower_volume f,D1) | k) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p1 implies p1 . i = ((lower_volume f,D1) | k) . i )
assume that
A118: 1 <= i and
A119: i <= len p1 ; :: thesis: p1 . i = ((lower_volume f,D1) | k) . i
A120: i in Seg (len p1) by A118, A119, FINSEQ_1:3;
then A121: i in dom ((lower_volume f,D1) | k) by A117, FINSEQ_1:def 3;
then A122: i in dom ((lower_volume f,D1) | (Seg k)) by FINSEQ_1:def 15;
k <= k + 1 by NAT_1:11;
then A123: Seg k c= Seg (k + 1) by FINSEQ_1:7;
A124: dom ((lower_volume f,D1) | (k + 1)) = Seg (len ((lower_volume f,D1) | (k + 1))) by FINSEQ_1:def 3
.= Seg (k + 1) by A109, FINSEQ_1:80 ;
dom ((lower_volume f,D1) | k) = Seg (len ((lower_volume f,D1) | k)) by FINSEQ_1:def 3
.= Seg k by A116, FINSEQ_1:80 ;
then i in dom ((lower_volume f,D1) | (k + 1)) by A121, A123, A124;
then A125: i in dom ((lower_volume f,D1) | (Seg (k + 1))) by FINSEQ_1:def 15;
A126: ((lower_volume f,D1) | (k + 1)) . i = ((lower_volume f,D1) | (Seg (k + 1))) . i by FINSEQ_1:def 15
.= (lower_volume f,D1) . i by A125, FUNCT_1:70 ;
A127: ((lower_volume f,D1) | k) . i = ((lower_volume f,D1) | (Seg k)) . i by FINSEQ_1:def 15
.= (lower_volume f,D1) . i by A122, FUNCT_1:70 ;
i in dom p1 by A120, FINSEQ_1:def 3;
hence p1 . i = ((lower_volume f,D1) | k) . i by A113, A127, A126, FINSEQ_1:def 7; :: thesis: verum

end;

then A128: p1 = (lower_volume f,D1) | k by A117, FINSEQ_1:18;
A129: indx D2,D1,(k + 1) in dom D2 by A1, A104, Def21;
then A130: indx D2,D1,(k + 1) in Seg (len D2) by FINSEQ_1:def 3;
then A131: 1 <= indx D2,D1,(k + 1) by FINSEQ_1:3;
not k + 1 is trivial by A108, NAT_2:def 1;
then k + 1 >= 2 by NAT_2:31;
then k >= (1 + 1) - 1 by XREAL_1:22;
then A132: k in Seg (len D1) by A115, FINSEQ_1:3;
then A133: k in dom D1 by FINSEQ_1:def 3;
then A134: indx D2,D1,k in dom D2 by A1, Def21;
A135: indx D2,D1,k < indx D2,D1,(k + 1)

proof

k < k + 1 by NAT_1:13;
then A136: D1 . k < D1 . (k + 1) by A104, A133, SEQM_3:def 1;
assume indx D2,D1,k >= indx D2,D1,(k + 1) ; :: thesis: contradiction
then A137: D2 . (indx D2,D1,k) >= D2 . (indx D2,D1,(k + 1)) by A134, A129, SEQ_4:154;
D1 . k = D2 . (indx D2,D1,k) by A1, A133, Def21;
hence contradiction by A1, A104, A137, A136, Def21; :: thesis: verum

end;

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

proof

assume indx D2,D1,(k + 1) < indx D2,D1,k ; :: thesis: contradiction
then A139: D2 . (indx D2,D1,(k + 1)) < D2 . (indx D2,D1,k) by A134, A129, SEQM_3:def 1;
D1 . (k + 1) = D2 . (indx D2,D1,(k + 1)) by A1, A104, Def21;
then D1 . (k + 1) < D1 . k by A1, A133, A139, Def21;
hence contradiction by A104, A133, NAT_1:11, SEQ_4:154; :: thesis: verum

end;

then consider ID being Nat such that
A140: indx D2,D1,(k + 1) = (indx D2,D1,k) + ID by NAT_1:10;
reconsider ID = ID as Element of NAT by ORDINAL1:def 13;
A141: len (lower_volume f,D2) = len D2 by Def8;
then A142: indx D2,D1,(k + 1) <= len (lower_volume f,D2) by A130, FINSEQ_1:3;
then len ((lower_volume f,D2) | (indx D2,D1,(k + 1))) = (indx D2,D1,k) + ((indx D2,D1,(k + 1)) - (indx D2,D1,k)) by FINSEQ_1:80;
then consider p2, q2 being FinSequence of REAL such that
A143: len p2 = indx D2,D1,k and
A144: len q2 = (indx D2,D1,(k + 1)) - (indx D2,D1,k) and
A145: (lower_volume f,D2) | (indx D2,D1,(k + 1)) = p2 ^ q2 by A140, FINSEQ_2:26;
A146: indx D2,D1,(k + 1) <= len D2 by A130, FINSEQ_1:3;
indx D2,D1,k in dom D2 by A1, A133, Def21;
then A147: indx D2,D1,k in Seg (len D2) by FINSEQ_1:def 3;
then A148: 1 <= indx D2,D1,k by FINSEQ_1:3;
A149: Sum q1 <= Sum q2

proof

set MD2 = mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1));
set MD1 = mid D1,(k + 1),(k + 1);
set DD1 = divset D1,(k + 1);
set g = f | (divset D1,(k + 1));
set S1 = divs (divset D1,(k + 1));
A150: 1 <= (indx D2,D1,k) + 1 by NAT_1:11;
reconsider g = f | (divset D1,(k + 1)) as PartFunc of (divset D1,(k + 1)),REAL by PARTFUN1:43;
(k + 1) - 1 = k ;
then A151: lower_bound (divset D1,(k + 1)) = D1 . k by A104, A108, Def5;
dom g = (dom f) /\ (divset D1,(k + 1)) by RELAT_1:90;
then dom g = A /\ (divset D1,(k + 1)) by FUNCT_2:def 1;
then dom g = divset D1,(k + 1) by A104, Th10, XBOOLE_1:28;
then A152: g is total by PARTFUN1:def 4;
A153: upper_bound (divset D1,(k + 1)) = D1 . (k + 1) by A104, A108, Def5;
A154: D2 . (indx D2,D1,(k + 1)) = D1 . (k + 1) by A1, A104, Def21;
A155: (indx D2,D1,k) + 1 <= indx D2,D1,(k + 1) by A135, NAT_1:13;
then A156: (indx D2,D1,k) + 1 <= len D2 by A146, XXREAL_0:2;
then (indx D2,D1,k) + 1 in Seg (len D2) by A150, FINSEQ_1:3;
then A157: (indx D2,D1,k) + 1 in dom D2 by FINSEQ_1:def 3;
then D2 . ((indx D2,D1,k) + 1) >= D2 . (indx D2,D1,k) by A134, NAT_1:11, SEQ_4:154;
then D2 . ((indx D2,D1,k) + 1) >= lower_bound (divset D1,(k + 1)) by A1, A133, A151, Def21;
then reconsider MD2 = mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1)) as Division of divset D1,(k + 1) by A129, A155, A157, A154, A153, Th39;
A158: ((indx D2,D1,(k + 1)) -' ((indx D2,D1,k) + 1)) + 1 = ((indx D2,D1,(k + 1)) - ((indx D2,D1,k) + 1)) + 1 by A155, XREAL_1:235
.= (indx D2,D1,(k + 1)) - (indx D2,D1,k) ;
A159: for n being Nat st 1 <= n & n <= len q2 holds
q2 . n = (lower_volume g,MD2) . n

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len q2 implies q2 . n = (lower_volume g,MD2) . n )
assume that
A160: 1 <= n and
A161: n <= len q2 ; :: thesis: q2 . n = (lower_volume g,MD2) . n
A162: n in Seg (len q2) by A160, A161, FINSEQ_1:3;
then A163: n in dom q2 by FINSEQ_1:def 3;
then A164: (indx D2,D1,k) + n in dom ((lower_volume f,D2) | (indx D2,D1,(k + 1))) by A143, A145, FINSEQ_1:41;
then A165: (indx D2,D1,k) + n in dom ((lower_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
A166: len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) = ID by A131, A146, A140, A155, A156, A150, A158, FINSEQ_6:124;
A167: dom ((lower_volume f,D2) | (indx D2,D1,(k + 1))) = Seg (len ((lower_volume f,D2) | (indx D2,D1,(k + 1)))) by FINSEQ_1:def 3
.= Seg (indx D2,D1,(k + 1)) by A142, FINSEQ_1:80 ;
then (indx D2,D1,k) + n <= indx D2,D1,(k + 1) by A164, FINSEQ_1:3;
then A168: n <= (indx D2,D1,(k + 1)) - (indx D2,D1,k) by XREAL_1:21;
then n in Seg (len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1)))) by A140, A160, A166, FINSEQ_1:3;
then A169: n in dom MD2 by FINSEQ_1:def 3;
A170: Seg (indx D2,D1,(k + 1)) c= Seg (len D2) by A146, FINSEQ_1:7;
then (indx D2,D1,k) + n in Seg (len D2) by A167, A164;
then A171: (indx D2,D1,k) + n in dom D2 by FINSEQ_1:def 3;
A172: q2 . n = ((lower_volume f,D2) | (indx D2,D1,(k + 1))) . ((indx D2,D1,k) + n) by A143, A145, A163, FINSEQ_1:def 7
.= ((lower_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) . ((indx D2,D1,k) + n) by FINSEQ_1:def 15
.= (lower_volume f,D2) . ((indx D2,D1,k) + n) by A165, FUNCT_1:70
.= (lower_bound (rng (f | (divset D2,((indx D2,D1,k) + n))))) * (vol (divset D2,((indx D2,D1,k) + n))) by A171, Def8 ;
A173: 1 <= (indx D2,D1,k) + n by A167, A164, FINSEQ_1:3;
A174: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )

proof

now

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

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

then A176: 1 <= (indx D2,D1,k) + 1 by A167, A164, FINSEQ_1:3;
A177: (indx D2,D1,k) + 1 <= len D2 by A167, A164, A170, A175, FINSEQ_1:3;
A178: upper_bound (divset MD2,1) = (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) . 1 by A169, A175, Def5
.= D2 . (1 + (indx D2,D1,k)) by A131, A146, A176, A177, FINSEQ_6:124 ;
A179: (indx D2,D1,k) + 1 <> 1 by A148, NAT_1:13;
A180: (k + 1) - 1 = k ;
A181: lower_bound (divset MD2,1) = lower_bound (divset D1,(k + 1)) by A169, A175, Def5
.= D1 . k by A104, A108, A180, Def5 ;
A182: divset D2,((indx D2,D1,k) + n) = [.(lower_bound (divset D2,((indx D2,D1,k) + 1))),(upper_bound (divset D2,((indx D2,D1,k) + 1))).] by A175, Th5
.= [.(D2 . (((indx D2,D1,k) + 1) - 1)),(upper_bound (divset D2,((indx D2,D1,k) + 1))).] by A157, A179, Def5
.= [.(D2 . (indx D2,D1,k)),(D2 . ((indx D2,D1,k) + 1)).] by A157, A179, Def5
.= [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A1, A133, Def21 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A175, A181, A178, Th5; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )
divset MD2,n = [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A175, A181, A178, Th5;
hence ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A169, A182, Th10; :: thesis: verum

end;

suppose A183: n <> 1 ; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )

A184: (indx D2,D1,k) + n <> 1

proof

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

end;

A185: divset D2,((indx D2,D1,k) + n) = [.(lower_bound (divset D2,((indx D2,D1,k) + n))),(upper_bound (divset D2,((indx D2,D1,k) + n))).] by Th5
.= [.(D2 . (((indx D2,D1,k) + n) - 1)),(upper_bound (divset D2,((indx D2,D1,k) + n))).] by A171, A184, Def5
.= [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A171, A184, Def5 ;
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:22;
then A186: n - 1 <= len MD2 by A140, A168, A166, XXREAL_0:2;
A187: (indx D2,D1,k) + 1 <= indx D2,D1,(k + 1) by A135, NAT_1:13;
not n is trivial by A160, A183, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:31;
then A188: 1 <= n - 1 by XREAL_1:21;
consider n1 being Nat such that
A189: n = 1 + n1 by A160, NAT_1:10;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 13;
A190: (n1 + ((indx D2,D1,k) + 1)) -' 1 = ((indx D2,D1,k) + n) - 1 by A173, A189, XREAL_1:235;
A191: (n + ((indx D2,D1,k) + 1)) -' 1 = ((n + (indx D2,D1,k)) + 1) - 1 by NAT_1:11, XREAL_1:235
.= (indx D2,D1,k) + n ;
A192: lower_bound (divset MD2,n) = MD2 . (n - 1) by A169, A183, Def5
.= D2 . (((indx D2,D1,k) + n) - 1) by A131, A146, A156, A150, A187, A189, A190, A188, A186, FINSEQ_6:124 ;
A193: upper_bound (divset MD2,n) = MD2 . n by A169, A183, Def5
.= D2 . ((indx D2,D1,k) + n) by A131, A146, A140, A156, A150, A160, A162, A168, A166, A187, A191, FINSEQ_6:124 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A192, A185, Th5; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )
divset MD2,n = [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A192, A193, Th5;
hence ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A169, A185, Th10; :: thesis: verum

end;

end;

end;

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

end;

then g | (divset MD2,n) = f | (divset D2,((indx D2,D1,k) + n)) by FUNCT_1:82;
hence q2 . n = (lower_volume g,MD2) . n by A169, A172, A174, Def8; :: thesis: verum

end;

(k + 1) - 1 = k ;
then A194: lower_bound (divset D1,(k + 1)) = D1 . k by A104, A108, Def5;
D1 . (k + 1) = upper_bound (divset D1,(k + 1)) by A104, A108, Def5;
then reconsider MD1 = mid D1,(k + 1),(k + 1) as Division of divset D1,(k + 1) by A104, A114, A133, A194, Th39, SEQ_4:154;
A195: g | (divset D1,(k + 1)) is bounded_below

proof

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

proof

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

end;

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

end;

len MD1 = ((k + 1) -' (k + 1)) + 1 by A106, A107, FINSEQ_6:124;
then A200: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
A201: for n being Nat st 1 <= n & n <= len q1 holds
q1 . n = (lower_volume g,MD1) . n

proof

k + 1 in Seg (len ((lower_volume f,D1) | (k + 1))) by A110, FINSEQ_1:6;
then k + 1 in dom ((lower_volume f,D1) | (k + 1)) by FINSEQ_1:def 3;
then A202: k + 1 in dom ((lower_volume f,D1) | (Seg (k + 1))) by FINSEQ_1:def 15;
A203: ((lower_volume f,D1) | (k + 1)) . (k + 1) = ((lower_volume f,D1) | (Seg (k + 1))) . (k + 1) by FINSEQ_1:def 15
.= (lower_volume f,D1) . (k + 1) by A202, FUNCT_1:70 ;
A204: MD1 . 1 = D1 . (k + 1) by A106, A107, FINSEQ_6:124;
1 in Seg 1 by FINSEQ_1:5;
then A205: 1 in dom MD1 by A200, FINSEQ_1:def 3;
then A206: upper_bound (divset MD1,1) = MD1 . 1 by Def5;
let n be Nat; :: thesis: ( 1 <= n & n <= len q1 implies q1 . n = (lower_volume g,MD1) . n )
assume that
A207: 1 <= n and
A208: n <= len q1 ; :: thesis: q1 . n = (lower_volume g,MD1) . n
A209: n = 1 by A112, A207, A208, XXREAL_0:1;
lower_bound (divset MD1,1) = lower_bound (divset D1,(k + 1)) by A205, Def5;
then A210: divset MD1,1 = [.(lower_bound (divset D1,(k + 1))),(D1 . (k + 1)).] by A206, A204, Th5;
(k + 1) - 1 = k ;
then A211: lower_bound (divset D1,(k + 1)) = D1 . k by A104, A108, Def5;
upper_bound (divset D1,(k + 1)) = D1 . (k + 1) by A104, A108, Def5;
then A212: divset D1,(k + 1) = [.(D1 . k),(D1 . (k + 1)).] by A211, Th5;
A213: n in Seg (len q1) by A207, A208, FINSEQ_1:3;
then n in dom MD1 by A112, A200, FINSEQ_1:def 3;
then A214: (lower_volume g,MD1) . n = (lower_bound (rng (g | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by A209, A210, A211, A212, Def8;
n in dom q1 by A213, FINSEQ_1:def 3;
then q1 . n = (lower_volume f,D1) . (k + 1) by A111, A113, A209, A203, FINSEQ_1:def 7
.= (lower_bound (rng (f | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by A104, Def8 ;
hence q1 . n = (lower_volume g,MD1) . n by A214, FUNCT_1:82; :: thesis: verum

end;

len q1 = len (lower_volume g,MD1) by A112, A200, Def8;
then A215: q1 = lower_volume g,MD1 by A201, FINSEQ_1:18;
len MD1 = ((k + 1) -' (k + 1)) + 1 by A106, A107, FINSEQ_6:124;
then len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
then A216: lower_sum g,MD1 <= lower_sum g,MD2 by A195, A152, Th33;
len (lower_volume g,MD2) = len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) by Def8
.= (indx D2,D1,(k + 1)) - (indx D2,D1,k) by A131, A146, A155, A156, A150, A158, FINSEQ_6:124 ;
hence Sum q1 <= Sum q2 by A144, A215, A159, A216, FINSEQ_1:18; :: thesis: verum

end;

set KD2 = (lower_volume f,D2) | (indx D2,D1,k);
A217: Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1))) = (Sum p2) + (Sum q2) by A145, RVSUM_1:105;
A218: indx D2,D1,k <= len (lower_volume f,D2) by A141, A147, FINSEQ_1:3;
then A219: len p2 = len ((lower_volume f,D2) | (indx D2,D1,k)) by A143, FINSEQ_1:80;
for i being Nat st 1 <= i & i <= len p2 holds
p2 . i = ((lower_volume f,D2) | (indx D2,D1,k)) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len p2 implies p2 . i = ((lower_volume f,D2) | (indx D2,D1,k)) . i )
assume that
A220: 1 <= i and
A221: i <= len p2 ; :: thesis: p2 . i = ((lower_volume f,D2) | (indx D2,D1,k)) . i
A222: i in Seg (len p2) by A220, A221, FINSEQ_1:3;
then A223: i in dom ((lower_volume f,D2) | (indx D2,D1,k)) by A219, FINSEQ_1:def 3;
then A224: i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,k))) by FINSEQ_1:def 15;
A225: dom ((lower_volume f,D2) | (indx D2,D1,(k + 1))) = Seg (len ((lower_volume f,D2) | (indx D2,D1,(k + 1)))) by FINSEQ_1:def 3
.= Seg (indx D2,D1,(k + 1)) by A142, FINSEQ_1:80 ;
A226: Seg (indx D2,D1,k) c= Seg (indx D2,D1,(k + 1)) by A138, FINSEQ_1:7;
dom ((lower_volume f,D2) | (indx D2,D1,k)) = Seg (len ((lower_volume f,D2) | (indx D2,D1,k))) by FINSEQ_1:def 3
.= Seg (indx D2,D1,k) by A218, FINSEQ_1:80 ;
then i in dom ((lower_volume f,D2) | (indx D2,D1,(k + 1))) by A223, A226, A225;
then A227: i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
A228: ((lower_volume f,D2) | (indx D2,D1,(k + 1))) . i = ((lower_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) . i by FINSEQ_1:def 15
.= (lower_volume f,D2) . i by A227, FUNCT_1:70 ;
A229: ((lower_volume f,D2) | (indx D2,D1,k)) . i = ((lower_volume f,D2) | (Seg (indx D2,D1,k))) . i by FINSEQ_1:def 15
.= (lower_volume f,D2) . i by A224, FUNCT_1:70 ;
i in dom p2 by A222, FINSEQ_1:def 3;
hence p2 . i = ((lower_volume f,D2) | (indx D2,D1,k)) . i by A145, A229, A228, FINSEQ_1:def 7; :: thesis: verum

end;

then A230: p2 = (lower_volume f,D2) | (indx D2,D1,k) by A219, FINSEQ_1:18;
Sum ((lower_volume f,D1) | (k + 1)) = (Sum p1) + (Sum q1) by A113, RVSUM_1:105;
then Sum q1 = (Sum ((lower_volume f,D1) | (k + 1))) - (Sum p1) ;
then Sum ((lower_volume f,D1) | (k + 1)) <= (Sum q2) + (Sum p1) by A149, XREAL_1:22;
then (Sum ((lower_volume f,D1) | (k + 1))) - (Sum q2) <= Sum p1 by XREAL_1:22;
then (Sum ((lower_volume f,D1) | (k + 1))) - (Sum q2) <= Sum p2 by A103, A132, A128, A230, FINSEQ_1:def 3, XXREAL_0:2;
hence Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1))) by A217, XREAL_1:22; :: thesis: verum

end;

end;

end;

hence Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1))) ; :: thesis: verum

end;

thus for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A3, A102); :: thesis: verum

end;

hence for i being non empty Element of NAT st i in dom D1 holds
Sum ((lower_volume f,D1) | i) <= Sum ((lower_volume f,D2) | (indx D2,D1,i)) ; :: thesis: verum