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

assume A4: 1 in dom D1 ; :: thesis: Sum ((lower_volume f,D1) | 1) <= Sum ((lower_volume f,D2) | (indx D2,D1,1))
then 1 in Seg (len D1) by FINSEQ_1:def 3;
then A6: 1 <= len D1 by FINSEQ_1:3;
then A7: len (mid D1,1,1) = (1 -' 1) + 1 by JORDAN3:27;
then A8: len (mid D1,1,1) = 1 by XREAL_1:237;
A9: mid D1,1,1 = D1 | 1

proof

A10: len (mid D1,1,1) = len (D1 | 1) by A6, 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 A11: ( 1 <= k & k <= len (mid D1,1,1) ) ; :: thesis: (mid D1,1,1) . k = (D1 | 1) . k
then A12: k = 1 by A8, XXREAL_0:1;
then A13: (mid D1,1,1) . k = D1 . ((1 + 1) - 1) by A6, JORDAN3:27;
k in Seg (len (D1 | 1)) by A10, A11, 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 (D1 | (Seg 1)) . k = D1 . k by FUNCT_1:70;
hence (mid D1,1,1) . k = (D1 | 1) . k by A12, A13, FINSEQ_1:def 15; :: thesis: verum

end;

hence mid D1,1,1 = D1 | 1 by A10, FINSEQ_1:18; :: thesis: verum

end;

indx D2,D1,1 in dom D2 by A1, A4, Def21;
then indx D2,D1,1 in Seg (len D2) by FINSEQ_1:def 3;
then A14: ( 1 <= indx D2,D1,1 & indx D2,D1,1 <= len D2 ) by FINSEQ_1:3;
then A15: 1 <= len D2 by XXREAL_0:2;
then len (mid D2,1,(indx D2,D1,1)) = ((indx D2,D1,1) -' 1) + 1 by A14, JORDAN3:27;
then A16: len (mid D2,1,(indx D2,D1,1)) = ((indx D2,D1,1) - 1) + 1 by A14, XREAL_1:235;
then A17: len (mid D2,1,(indx D2,D1,1)) = len (D2 | (indx D2,D1,1)) by A14, FINSEQ_1:80;
A18: 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 A19: ( 1 <= k & k <= len (mid D2,1,(indx D2,D1,1)) ) ; :: thesis: (mid D2,1,(indx D2,D1,1)) . k = (D2 | (indx D2,D1,1)) . k
then A20: k in Seg (len (D2 | (indx D2,D1,1))) by A17, FINSEQ_1:3;
then (mid D2,1,(indx D2,D1,1)) . k = D2 . ((k + 1) -' 1) by A14, A15, A19, JORDAN3:27;
then A21: (mid D2,1,(indx D2,D1,1)) . k = D2 . ((k + 1) - 1) by NAT_1:11, XREAL_1:235;
k in dom (D2 | (indx D2,D1,1)) by A20, FINSEQ_1:def 3;
then k in dom (D2 | (Seg (indx D2,D1,1))) by FINSEQ_1:def 15;
then (D2 | (Seg (indx D2,D1,1))) . k = D2 . k by FUNCT_1:70;
hence (mid D2,1,(indx D2,D1,1)) . k = (D2 | (indx D2,D1,1)) . k by A21, FINSEQ_1:def 15; :: thesis: verum

end;

then A22: mid D2,1,(indx D2,D1,1) = D2 | (indx D2,D1,1) by A17, FINSEQ_1:18;
set DD1 = mid D1,1,1;
set DD2 = mid D2,1,(indx D2,D1,1);
set B = divset D1,1;
set S1 = divs (divset D1,1);
A23: D1 . 1 = upper_bound (divset D1,1) by A4, Def5;
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 A4, A23, Th39;
A24: indx D2,D1,1 in dom D2 by A1, A4, Def21;
then indx D2,D1,1 in Seg (len D2) by FINSEQ_1:def 3;
then A25: ( 1 <= indx D2,D1,1 & indx D2,D1,1 <= len D2 ) by FINSEQ_1:3;
then 1 <= len D2 by XXREAL_0:2;
then 1 in Seg (len D2) by FINSEQ_1:3;
then A26: 1 in dom D2 by FINSEQ_1:def 3;
A27: D2 . (indx D2,D1,1) = upper_bound (divset D1,1) by A1, A4, A23, Def21;
A28: rng D2 c= A by Def2;
D2 . 1 in rng D2 by A26, FUNCT_1:def 5;
then D2 . 1 in A by A28;
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 A4, Def5;
then reconsider DD2 = mid D2,1,(indx D2,D1,1) as Division of divset D1,1 by A24, A25, A26, A27, Th39;
set g = f | (divset D1,1);
reconsider g = f | (divset D1,1) as PartFunc of (divset D1,1),REAL by PARTFUN1:43;
A29: dom g = (dom f) /\ (divset D1,1) by RELAT_1:90;
then dom g = A /\ (divset D1,1) by FUNCT_2:def 1;
then dom g = divset D1,1 by A4, Th10, XBOOLE_1:28;
then g is total by PARTFUN1:def 4;
then A30: g is Function of (divset D1,1),REAL ;
g | (divset D1,1) is bounded_below

proof

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

end;

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

end;

then A35: lower_sum g,DD1 <= lower_sum g,DD2 by A8, A30, Th33;
A36: lower_volume g,DD1 = (lower_volume f,D1) | 1

proof

A37: len (lower_volume g,DD1) = len DD1 by Def8
.= 1 by A7, XREAL_1:237 ;
1 <= len (lower_volume f,D1) by A6, Def8;
then A38: len (lower_volume g,DD1) = len ((lower_volume f,D1) | 1) by A37, FINSEQ_1:80;
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 A39: ( 1 <= i & i <= len (lower_volume g,DD1) ) ; :: thesis: (lower_volume g,DD1) . i = ((lower_volume f,D1) | 1) . i
A40: len DD1 = 1 by A7, XREAL_1:237;
A41: 1 in Seg 1 by FINSEQ_1:5;
A43: 1 in dom DD1 by A40, A41, FINSEQ_1:def 3;
A44: 1 in dom (D1 | (Seg 1))

proof

dom (D1 | (Seg 1)) = (dom D1) /\ (Seg 1) by RELAT_1:90;
hence 1 in dom (D1 | (Seg 1)) by A4, A41, XBOOLE_0:def 4; :: thesis: verum

end;

A45: (lower_volume g,DD1) . i = (lower_volume g,DD1) . 1 by A37, A39, XXREAL_0:1
.= (lower_bound (rng (g | (divset DD1,1)))) * (vol (divset DD1,1)) by A43, Def8 ;
A46: 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 A43, Def5
.= [.(lower_bound (divset D1,1)),(DD1 . 1).] by A43, Def5
.= [.(lower_bound A),((D1 | 1) . 1).] by A4, A9, Def5
.= [.(lower_bound A),((D1 | (Seg 1)) . 1).] by FINSEQ_1:def 15
.= [.(lower_bound A),(D1 . 1).] by A44, FUNCT_1:70 ;
A47: divset D1,1 = [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by Th5
.= [.(lower_bound A),(upper_bound (divset D1,1)).] by A4, Def5
.= [.(lower_bound A),(D1 . 1).] by A4, Def5 ;
dom (lower_volume f,D1) = Seg (len (lower_volume f,D1)) by FINSEQ_1:def 3
.= Seg (len D1) by Def8 ;
then dom ((lower_volume f,D1) | (Seg 1)) = (Seg (len D1)) /\ (Seg 1) by RELAT_1:90
.= Seg 1 by A6, FINSEQ_1:9 ;
then A48: 1 in dom ((lower_volume f,D1) | (Seg 1)) by FINSEQ_1:5;
((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 A37, A39, XXREAL_0:1
.= (lower_volume f,D1) . 1 by A48, FUNCT_1:70
.= (lower_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)) by Def8, A4 ;
hence (lower_volume g,DD1) . i = ((lower_volume f,D1) | 1) . i by A29, A45, A46, A47, RELAT_1:97; :: thesis: verum

end;

hence lower_volume g,DD1 = (lower_volume f,D1) | 1 by A38, FINSEQ_1:18; :: thesis: verum

end;

lower_volume g,DD2 = (lower_volume f,D2) | (indx D2,D1,1)

proof

A49: len (lower_volume g,DD2) = indx D2,D1,1 by A16, Def8;
indx D2,D1,1 <= len (lower_volume f,D2) by A14, Def8;
then A50: len (lower_volume g,DD2) = len ((lower_volume f,D2) | (indx D2,D1,1)) by A49, FINSEQ_1:80;
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 A51: ( 1 <= i & i <= len (lower_volume g,DD2) ) ; :: thesis: (lower_volume g,DD2) . i = ((lower_volume f,D2) | (indx D2,D1,1)) . i
A52: ( 1 <= i & i <= len DD2 & i in Seg (len DD2) & i in dom DD2 )

proof

thus ( 1 <= i & i <= len DD2 ) by A51, Def8; :: thesis: ( i in Seg (len DD2) & i in dom DD2 )
hence i in Seg (len DD2) by FINSEQ_1:3; :: thesis: i in dom DD2
hence i in dom DD2 by FINSEQ_1:def 3; :: thesis: verum

end;

divset DD2,i = divset D2,i

proof

A53: ( i in dom DD2 & i in dom D2 )

proof

thus i in dom DD2 by A52; :: thesis: i in dom D2
Seg (indx D2,D1,1) c= Seg (len D2) by A14, FINSEQ_1:7;
then i in Seg (len D2) by A16, A52;
hence i in dom D2 by FINSEQ_1:def 3; :: thesis: verum

end;

now

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

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

then A55: 1 in dom (D2 | (Seg (indx D2,D1,1))) by A22, A53, FINSEQ_1:def 15;
then 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by RELAT_1:90;
then A56: 1 in dom D2 by XBOOLE_0:def 4;
A57: divset DD2,i = [.(lower_bound (divset DD2,1)),(upper_bound (divset DD2,1)).] by A54, Th5
.= [.(lower_bound (divset D1,1)),(upper_bound (divset DD2,1)).] by A53, A54, Def5
.= [.(lower_bound (divset D1,1)),(DD2 . 1).] by A53, A54, Def5
.= [.(lower_bound (divset D1,1)),((D2 | (indx D2,D1,1)) . 1).] by A18, A52, A54
.= [.(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 A55, FUNCT_1:70
.= [.(lower_bound A),(D2 . 1).] by A4, Def5 ;
divset D2,i = [.(lower_bound (divset D2,1)),(upper_bound (divset D2,1)).] by A54, Th5
.= [.(lower_bound A),(upper_bound (divset D2,1)).] by A56, Def5
.= [.(lower_bound A),(D2 . 1).] by A56, Def5 ;
hence divset DD2,i = divset D2,i by A57; :: thesis: verum

end;

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

A59: DD2 . (i - 1) = D2 . (i - 1)

proof

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

proof

consider j being Nat such that
A61: i = 1 + j by A52, NAT_1:10;
not i is trivial by A52, A58, NAT_2:def 1;
then A62: ( i >= 1 + 1 & i - 1 <= (indx D2,D1,1) - 0 ) by A16, A52, NAT_2:31, XREAL_1:15;
then ( i - 1 >= 1 & i - 1 <= indx D2,D1,1 ) by XREAL_1:21;
then A63: i - 1 in Seg (indx D2,D1,1) by A61, FINSEQ_1:3;
( 1 <= i - 1 & i - 1 <= len D2 ) by A25, A62, XREAL_1:21, XXREAL_0:2;
then i - 1 in Seg (len D2) by A61, FINSEQ_1:3;
then i - 1 in dom D2 by FINSEQ_1:def 3;
then i - 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by A63, 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 A17, A18, FINSEQ_1:18
.= (D2 | (Seg (indx D2,D1,1))) . (i - 1) by FINSEQ_1:def 15 ;
hence DD2 . (i - 1) = D2 . (i - 1) by A60, FUNCT_1:70; :: thesis: verum

end;

A64: DD2 . i = D2 . i

proof

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

proof

( 1 <= i & i <= len D2 ) by A16, A25, A52, XXREAL_0:2;
then i in Seg (len D2) by FINSEQ_1:3;
then i in dom D2 by FINSEQ_1:def 3;
then i in (dom D2) /\ (Seg (indx D2,D1,1)) by A16, A52, XBOOLE_0:def 4;
hence i in dom (D2 | (Seg (indx D2,D1,1))) by RELAT_1:90; :: thesis: verum

end;

DD2 . i = (D2 | (indx D2,D1,1)) . i by A17, A18, FINSEQ_1:18
.= (D2 | (Seg (indx D2,D1,1))) . i by FINSEQ_1:def 15 ;
hence DD2 . i = D2 . i by A65, FUNCT_1:70; :: thesis: verum

end;

A66: divset DD2,i = [.(lower_bound (divset DD2,i)),(upper_bound (divset DD2,i)).] by Th5
.= [.(DD2 . (i - 1)),(upper_bound (divset DD2,i)).] by A53, A58, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A53, A58, A59, A64, Def5 ;
divset D2,i = [.(lower_bound (divset D2,i)),(upper_bound (divset D2,i)).] by Th5
.= [.(D2 . (i - 1)),(upper_bound (divset D2,i)).] by A53, A58, Def5
.= [.(D2 . (i - 1)),(D2 . i).] by A53, A58, Def5 ;
hence divset DD2,i = divset D2,i by A66; :: thesis: verum

end;

end;

end;

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

end;

then A67: (lower_volume g,DD2) . i = (lower_bound (rng (g | (divset D2,i)))) * (vol (divset D2,i)) by A52, Def8;
A68: divset D2,i c= divset D1,1

proof

A69: divset D2,i = [.(lower_bound (divset D2,i)),(upper_bound (divset D2,i)).] by Th5;
A70: divset D1,1 = [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by Th5;
( 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)).] )

proof

A71: ( i in dom DD2 & i in dom D2 )

proof

thus i in dom DD2 by A52; :: thesis: i in dom D2
Seg (indx D2,D1,1) c= Seg (len D2) by A14, FINSEQ_1:7;
then i in Seg (len D2) by A16, A52;
hence i in dom D2 by FINSEQ_1:def 3; :: thesis: verum

end;

now

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

suppose A72: 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 A22, A71, FINSEQ_1:def 15;
then 1 in (dom D2) /\ (Seg (indx D2,D1,1)) by RELAT_1:90;
then A73: 1 in dom D2 by XBOOLE_0:def 4;
then lower_bound (divset D2,i) = lower_bound A by A72, Def5;
then A74: lower_bound (divset D2,i) = lower_bound (divset D1,1) by A4, Def5;
lower_bound (divset D1,1) <= upper_bound (divset D1,1)

proof

ex a, b being Real st
( a <= b & a = lower_bound (divset D1,1) & b = upper_bound (divset D1,1) ) by Th4;
hence lower_bound (divset D1,1) <= upper_bound (divset D1,1) ; :: thesis: verum

end;

hence lower_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by A74, XXREAL_1:1; :: thesis: upper_bound (divset D2,i) in [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).]
A75: upper_bound (divset D2,i) = D2 . 1 by A72, A73, Def5;
D2 . 1 <= D2 . (indx D2,D1,1) by A24, A25, A73, GOBOARD2:18;
then D2 . 1 <= D1 . 1 by A1, A4, Def21;
then A76: upper_bound (divset D2,i) <= upper_bound (divset D1,1) by A4, A75, Def5;
lower_bound (divset D2,i) <= upper_bound (divset D2,i)

proof

ex a, b being Real st
( a <= b & a = lower_bound (divset D2,i) & b = upper_bound (divset D2,i) ) by Th4;
hence lower_bound (divset D2,i) <= upper_bound (divset D2,i) ; :: thesis: verum

end;

then consider a being Real such that
A77: ( a = upper_bound (divset D2,i) & lower_bound (divset D1,1) <= a & a <= upper_bound (divset D1,1) ) by A74, A76;
upper_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by A77;
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 A78: 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)).] )

consider j being Nat such that
A79: i = 1 + j by A52, NAT_1:10;
not i is trivial by A52, A78, NAT_2:def 1;
then A80: ( i >= 1 + 1 & i - 1 <= (indx D2,D1,1) - 0 ) by A16, A52, NAT_2:31, XREAL_1:15;
then ( 1 <= i - 1 & i - 1 <= len D2 ) by A25, XREAL_1:21, XXREAL_0:2;
then i - 1 in Seg (len D2) by A79, FINSEQ_1:3;
then A81: i - 1 in dom D2 by FINSEQ_1:def 3;
A83: lower_bound (divset D2,i) = D2 . (i - 1) by A71, A78, Def5;
A84: upper_bound (divset D2,i) = D2 . i by A71, A78, Def5;
A85: lower_bound (divset D1,1) = lower_bound A by A4, Def5;
A86: upper_bound (divset D1,1) = D1 . 1 by A4, Def5;
A87: rng D2 c= A by Def2;
D2 . (i - 1) in rng D2 by A81, FUNCT_1:def 5;
then A88: lower_bound (divset D2,i) >= lower_bound (divset D1,1) by A83, A85, A87, SEQ_4:def 5;
D2 . (i - 1) <= D2 . (indx D2,D1,1) by A24, A80, A81, GOBOARD2:18;
then lower_bound (divset D2,i) <= upper_bound (divset D1,1) by A1, A4, A83, A86, Def21;
then consider a being Real such that
A89: ( a = lower_bound (divset D2,i) & lower_bound (divset D1,1) <= a & a <= upper_bound (divset D1,1) ) by A88;
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)).]
D2 . i in rng D2 by A71, FUNCT_1:def 5;
then A90: upper_bound (divset D2,i) >= lower_bound (divset D1,1) by A84, A85, A87, SEQ_4:def 5;
D2 . i <= D2 . (indx D2,D1,1) by A16, A24, A52, A71, GOBOARD2:18;
then upper_bound (divset D2,i) <= upper_bound (divset D1,1) by A1, A4, A84, A86, Def21;
then consider a being Real such that
A91: ( a = upper_bound (divset D2,i) & lower_bound (divset D1,1) <= a & a <= upper_bound (divset D1,1) ) by A90;
upper_bound (divset D2,i) in { r where r is Real : ( lower_bound (divset D1,1) <= r & r <= upper_bound (divset D1,1) ) } by A91;
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;

hence ( 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)).] ) ; :: thesis: verum

end;

hence divset D2,i c= divset D1,1 by A69, A70, XXREAL_2:def 12; :: thesis: verum

end;

A92: ( i in dom D2 & i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,1))) )

proof

A93: Seg (indx D2,D1,1) c= Seg (len D2) by A14, FINSEQ_1:7;
then i in Seg (len D2) by A16, A52;
hence i in dom D2 by FINSEQ_1:def 3; :: thesis: i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,1)))
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 A93, XBOOLE_1:28 ;
hence i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,1))) by A16, A52; :: thesis: verum

end;

((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 A92, FUNCT_1:70
.= (lower_bound (rng (f | (divset D2,i)))) * (vol (divset D2,i)) by A92, Def8 ;
hence (lower_volume g,DD2) . i = ((lower_volume f,D2) | (indx D2,D1,1)) . i by A67, A68, FUNCT_1:82; :: thesis: verum

end;

hence lower_volume g,DD2 = (lower_volume f,D2) | (indx D2,D1,1) by A50, FINSEQ_1:18; :: thesis: verum

end;

hence Sum ((lower_volume f,D1) | 1) <= Sum ((lower_volume f,D2) | (indx D2,D1,1)) by A35, A36; :: thesis: verum

end;

A94: 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 A95: ( 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 A96: k + 1 in dom D1 ; :: thesis: Sum ((lower_volume f,D1) | (k + 1)) <= Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1)))
then k + 1 in Seg (len D1) by FINSEQ_1:def 3;
then A98: ( 1 <= k + 1 & k + 1 <= len D1 ) by 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, A96; :: thesis: verum

end;

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

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

proof

assume indx D2,D1,k >= indx D2,D1,(k + 1) ; :: thesis: contradiction
then A113: D2 . (indx D2,D1,k) >= D2 . (indx D2,D1,(k + 1)) by A107, A108, GOBOARD2:18;
k < k + 1 by NAT_1:13;
then A114: D1 . k < D1 . (k + 1) by A96, A104, SEQM_3:def 1;
D1 . k = D2 . (indx D2,D1,k) by A1, A104, Def21;
hence contradiction by A1, A96, A113, A114, Def21; :: thesis: verum

end;

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

proof

assume indx D2,D1,(k + 1) < indx D2,D1,k ; :: thesis: contradiction
then A116: D2 . (indx D2,D1,(k + 1)) < D2 . (indx D2,D1,k) by A107, A108, SEQM_3:def 1;
D1 . (k + 1) = D2 . (indx D2,D1,(k + 1)) by A1, A96, Def21;
then D1 . (k + 1) < D1 . k by A1, A104, A116, Def21;
hence contradiction by A96, A104, GOBOARD2:18, NAT_1:11; :: thesis: verum

end;

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

proof

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

end;

hence p1 = (lower_volume f,D1) | k by A124, FINSEQ_1:18; :: thesis: verum

end;

A133: p2 = (lower_volume f,D2) | (indx D2,D1,k)

proof

A134: len p2 = len ((lower_volume f,D2) | (indx D2,D1,k)) by A119, A122, 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 ( 1 <= i & i <= len p2 ) ; :: thesis: p2 . i = ((lower_volume f,D2) | (indx D2,D1,k)) . i
then A135: i in Seg (len p2) by FINSEQ_1:3;
then A136: i in dom p2 by FINSEQ_1:def 3;
A137: i in dom ((lower_volume f,D2) | (indx D2,D1,k)) by A134, A135, FINSEQ_1:def 3;
then A138: i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,k))) by FINSEQ_1:def 15;
A139: ((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 A138, FUNCT_1:70 ;
A140: 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 A119, FINSEQ_1:80 ;
A141: Seg (indx D2,D1,k) c= Seg (indx D2,D1,(k + 1)) by A115, FINSEQ_1:7;
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 A111, FINSEQ_1:80 ;
then i in dom ((lower_volume f,D2) | (indx D2,D1,(k + 1))) by A137, A140, A141;
then A142: i in dom ((lower_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
((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 A142, FUNCT_1:70 ;
hence p2 . i = ((lower_volume f,D2) | (indx D2,D1,k)) . i by A122, A136, A139, FINSEQ_1:def 7; :: thesis: verum

end;

hence p2 = (lower_volume f,D2) | (indx D2,D1,k) by A134, FINSEQ_1:18; :: thesis: verum

end;

A143: 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));
A144: ( 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 A96, A99, 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 A96, A99, A101, A104, Def5, GOBOARD2:18; :: thesis: verum

end;

then reconsider MD1 = mid D1,(k + 1),(k + 1) as Division of divset D1,(k + 1) by Th39;
A145: (indx D2,D1,k) + 1 <= indx D2,D1,(k + 1) by A112, NAT_1:13;
then A146: (indx D2,D1,k) + 1 <= len D2 by A110, XXREAL_0:2;
A147: 1 <= (indx D2,D1,k) + 1 by NAT_1:11;
then (indx D2,D1,k) + 1 in Seg (len D2) by A146, FINSEQ_1:3;
then A148: (indx D2,D1,k) + 1 in dom D2 by FINSEQ_1:def 3;
A149: D2 . (indx D2,D1,(k + 1)) = D1 . (k + 1) by A1, A96, Def21;
A150: ( lower_bound (divset D1,(k + 1)) = D1 . ((k + 1) - 1) & upper_bound (divset D1,(k + 1)) = D1 . (k + 1) ) by A96, A99, Def5;
(k + 1) - 1 = k ;
then A151: lower_bound (divset D1,(k + 1)) = D1 . k by A96, A99, Def5;
D2 . ((indx D2,D1,k) + 1) >= D2 . (indx D2,D1,k) by A107, A148, GOBOARD2:18, NAT_1:11;
then D2 . ((indx D2,D1,k) + 1) >= lower_bound (divset D1,(k + 1)) by A1, A104, 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 A108, A145, A148, A149, A150, Th39;
reconsider g = f | (divset D1,(k + 1)) as PartFunc of (divset D1,(k + 1)),REAL by PARTFUN1:43;
A152: ( g is total & g | (divset D1,(k + 1)) is bounded_below )

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

proof

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

end;

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

end;

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

end;

A158: q1 = lower_volume g,MD1

proof

len MD1 = ((k + 1) -' (k + 1)) + 1 by A98, JORDAN3:27;
then A159: len MD1 = ((k + 1) - (k + 1)) + 1 by XREAL_1:235;
then A160: len q1 = len (lower_volume g,MD1) by A121, Def8;
for n being Nat st 1 <= n & n <= len q1 holds
q1 . n = (lower_volume g,MD1) . n

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len q1 implies q1 . n = (lower_volume g,MD1) . n )
assume A161: ( 1 <= n & n <= len q1 ) ; :: thesis: q1 . n = (lower_volume g,MD1) . n
then A162: n = 1 by A121, XXREAL_0:1;
U: n in Seg (len q1) by A161, FINSEQ_1:3;
then A164: n in dom q1 by FINSEQ_1:def 3;
Y: n in dom MD1 by A121, A159, U, FINSEQ_1:def 3;
k + 1 in Seg (len ((lower_volume f,D1) | (k + 1))) by A120, FINSEQ_1:6;
then k + 1 in dom ((lower_volume f,D1) | (k + 1)) by FINSEQ_1:def 3;
then A165: k + 1 in dom ((lower_volume f,D1) | (Seg (k + 1))) by FINSEQ_1:def 15;
((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 A165, FUNCT_1:70 ;
then A166: q1 . n = (lower_volume f,D1) . (k + 1) by A121, A162, A164, FINSEQ_1:def 7
.= (lower_bound (rng (f | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by Def8, A96 ;
1 in dom MD1

proof

1 in Seg 1 by FINSEQ_1:5;
hence 1 in dom MD1 by A159, FINSEQ_1:def 3; :: thesis: verum

end;

then A167: ( lower_bound (divset MD1,1) = lower_bound (divset D1,(k + 1)) & upper_bound (divset MD1,1) = MD1 . 1 ) by Def5;
MD1 . 1 = D1 . (k + 1) by A98, JORDAN3:27;
then A168: divset MD1,1 = [.(lower_bound (divset D1,(k + 1))),(D1 . (k + 1)).] by A167, Th5;
(k + 1) - 1 = k ;
then A169: lower_bound (divset D1,(k + 1)) = D1 . k by A96, A99, Def5;
upper_bound (divset D1,(k + 1)) = D1 . (k + 1) by A96, A99, Def5;
then divset D1,(k + 1) = [.(D1 . k),(D1 . (k + 1)).] by A169, Th5;
then (lower_volume g,MD1) . n = (lower_bound (rng (g | (divset D1,(k + 1))))) * (vol (divset D1,(k + 1))) by A162, A168, A169, Def8, Y;
hence q1 . n = (lower_volume g,MD1) . n by A166, FUNCT_1:82; :: thesis: verum

end;

hence q1 = lower_volume g,MD1 by A160, FINSEQ_1:18; :: thesis: verum

end;

A170: q2 = lower_volume g,MD2

proof

A171: ((indx D2,D1,(k + 1)) -' ((indx D2,D1,k) + 1)) + 1 = ((indx D2,D1,(k + 1)) - ((indx D2,D1,k) + 1)) + 1 by A145, XREAL_1:235
.= (indx D2,D1,(k + 1)) - (indx D2,D1,k) ;
A172: 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 A110, A145, A146, A147, A171, JORDAN3:27 ;
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 A173: ( 1 <= n & n <= len q2 ) ; :: thesis: q2 . n = (lower_volume g,MD2) . n
then A174: n in Seg (len q2) by FINSEQ_1:3;
then A175: n in dom q2 by FINSEQ_1:def 3;
A176: 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 A111, FINSEQ_1:80 ;
A177: (indx D2,D1,k) + n in dom ((lower_volume f,D2) | (indx D2,D1,(k + 1))) by A122, A175, FINSEQ_1:41;
then A178: (indx D2,D1,k) + n in dom ((lower_volume f,D2) | (Seg (indx D2,D1,(k + 1)))) by FINSEQ_1:def 15;
A179: Seg (indx D2,D1,(k + 1)) c= Seg (len D2) by A110, FINSEQ_1:7;
then (indx D2,D1,k) + n in Seg (len D2) by A176, A177;
then A180: (indx D2,D1,k) + n in dom D2 by FINSEQ_1:def 3;
A181: ( 1 <= (indx D2,D1,k) + n & (indx D2,D1,k) + n <= indx D2,D1,(k + 1) ) by A176, A177, FINSEQ_1:3;
then A182: n <= (indx D2,D1,(k + 1)) - (indx D2,D1,k) by XREAL_1:21;
A183: len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) = ID by A110, A117, A145, A146, A147, A171, JORDAN3:27;
then n in Seg (len (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1)))) by A117, A173, A182, FINSEQ_1:3;
then A185: n in dom MD2 by FINSEQ_1:def 3;
A186: q2 . n = ((lower_volume f,D2) | (indx D2,D1,(k + 1))) . ((indx D2,D1,k) + n) by A122, A175, 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 A178, FUNCT_1:70
.= (lower_bound (rng (f | (divset D2,((indx D2,D1,k) + n))))) * (vol (divset D2,((indx D2,D1,k) + n))) by Def8, A180 ;
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

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) )

A189: (k + 1) - 1 = k ;
A190: ( 1 <= (indx D2,D1,k) + 1 & (indx D2,D1,k) + 1 <= len D2 ) by A176, A177, A179, A188, FINSEQ_1:3;
A191: (indx D2,D1,k) + 1 <> 1 by A119, NAT_1:13;
A192: lower_bound (divset MD2,1) = lower_bound (divset D1,(k + 1)) by A185, A188, Def5
.= D1 . k by A96, A99, A189, Def5 ;
A193: upper_bound (divset MD2,1) = (mid D2,((indx D2,D1,k) + 1),(indx D2,D1,(k + 1))) . 1 by A185, A188, Def5
.= D2 . (1 + (indx D2,D1,k)) by A110, A190, JORDAN3:27 ;
then A194: divset MD2,n = [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A188, A192, Th5;
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, Th5
.= [.(D2 . (((indx D2,D1,k) + 1) - 1)),(upper_bound (divset D2,((indx D2,D1,k) + 1))).] by A148, A191, Def5
.= [.(D2 . (indx D2,D1,k)),(D2 . ((indx D2,D1,k) + 1)).] by A148, A191, Def5
.= [.(D1 . k),(D2 . ((indx D2,D1,k) + 1)).] by A1, A104, Def21 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A188, A192, A193, Th5; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )
thus ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A185, A194, A195, Th10; :: 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) + 1 <= indx D2,D1,(k + 1) by A112, NAT_1:13;
consider n1 being Nat such that
A198: n = 1 + n1 by A173, NAT_1:10;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 13;
A199: (n1 + ((indx D2,D1,k) + 1)) -' 1 = ((indx D2,D1,k) + n) - 1 by A181, A198, XREAL_1:235;
A200: ( 1 <= n - 1 & n - 1 <= len MD2 )

proof

not n is trivial by A173, A196, NAT_2:def 1;
then n >= 1 + 1 by NAT_2:31;
hence n - 1 >= 1 by XREAL_1:21; :: thesis: n - 1 <= len MD2
n <= n + 1 by NAT_1:12;
then n - 1 <= n by XREAL_1:22;
hence n - 1 <= len MD2 by A117, A182, A183, XXREAL_0:2; :: thesis: verum

end;

A201: (n + ((indx D2,D1,k) + 1)) -' 1 = (indx D2,D1,k) + n

proof

(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 ;
hence (n + ((indx D2,D1,k) + 1)) -' 1 = (indx D2,D1,k) + n ; :: thesis: verum

end;

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

end;

A203: lower_bound (divset MD2,n) = MD2 . (n - 1) by A185, A196, Def5
.= D2 . (((indx D2,D1,k) + n) - 1) by A110, A146, A147, A197, A198, A199, A200, JORDAN3:27 ;
A204: upper_bound (divset MD2,n) = MD2 . n by A185, A196, Def5
.= D2 . ((indx D2,D1,k) + n) by A110, A117, A146, A147, A173, A174, A182, A183, A197, A201, JORDAN3:27 ;
then A205: divset MD2,n = [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A203, Th5;
A206: 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 A180, A202, Def5
.= [.(D2 . (((indx D2,D1,k) + n) - 1)),(D2 . ((indx D2,D1,k) + n)).] by A180, A202, Def5 ;
hence divset MD2,n = divset D2,((indx D2,D1,k) + n) by A203, A204, Th5; :: thesis: ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) )
thus ( divset MD2,n = divset D2,((indx D2,D1,k) + n) & divset D2,((indx D2,D1,k) + n) c= divset D1,(k + 1) ) by A185, A205, A206, 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 A186, A187, Def8, A185; :: thesis: verum

end;

hence q2 = lower_volume g,MD2 by A122, A172, FINSEQ_1:18; :: thesis: verum

end;

( len MD1 = 1 & MD1 <= MD2 )

proof

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

end;

then lower_sum g,MD1 <= lower_sum g,MD2 by A152, Th33;
hence Sum q1 <= Sum q2 by A158, A170; :: thesis: verum

end;

A207: Sum ((lower_volume f,D1) | (k + 1)) = (Sum p1) + (Sum q1) by A121, RVSUM_1:105;
A208: Sum ((lower_volume f,D2) | (indx D2,D1,(k + 1))) = (Sum p2) + (Sum q2) by A122, RVSUM_1:105;
Sum q1 = (Sum ((lower_volume f,D1) | (k + 1))) - (Sum p1) by A207;
then Sum ((lower_volume f,D1) | (k + 1)) <= (Sum q2) + (Sum p1) by A143, 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 A95, A103, A123, A133, 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 A208, 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, A94); :: 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