let r be Real; :: thesis:
let i, j be Element of NAT ; :: thesis:
let A be closed-interval Subset of REAL ; :: thesis:
let D1, D2 be Division of A; :: thesis:
assume A1: i in dom D1 ; :: thesis:
assume A2: j in dom D1 ; :: thesis:
assume A3: i <= j ; :: thesis:
assume A4: D1 <= D2 ; :: thesis:
assume A5: r < (mid D2,(indx D2,D1,i),(indx D2,D1,j)) . 1 ; :: thesis:
set MD1 = mid D1,i,j;
set MD2 = mid D2,(indx D2,D1,i),(indx D2,D1,j);
A6: ( indx D2,D1,i in dom D2 & D2 . (indx D2,D1,i) = D1 . i ) by A1, A4, INTEGRA1:def 21;
A7: ( indx D2,D1,j in dom D2 & D2 . (indx D2,D1,j) = D1 . j ) by A2, A4, INTEGRA1:def 21;
D1 . i <= D1 . j by A1, A2, A3, GOBOARD2:18;
then A8: indx D2,D1,i <= indx D2,D1,j by A6, A7, SEQM_3:def 1;
then consider B being closed-interval Subset of REAL such that
A9: ( r = lower_bound B & upper_bound B = (mid D2,(indx D2,D1,i),(indx D2,D1,j)) . (len (mid D2,(indx D2,D1,i),(indx D2,D1,j))) & len (mid D2,(indx D2,D1,i),(indx D2,D1,j)) = ((indx D2,D1,j) - (indx D2,D1,i)) + 1 & mid D2,(indx D2,D1,i),(indx D2,D1,j) is Division of B ) by A5, A6, A7, Th11;
reconsider MD2 = mid D2,(indx D2,D1,i),(indx D2,D1,j) as Division of B by A9, INTEGRA1:def 3;
(indx D2,D1,j) - (indx D2,D1,i) >= 0 by A8, XREAL_1:50;
then A10: ((indx D2,D1,j) - (indx D2,D1,i)) + 1 >= 0 + 1 by XREAL_1:8;
A11: ( 1 <= indx D2,D1,i & indx D2,D1,j <= len D2 ) by A6, A7, FINSEQ_3:27;
then A12: MD2 . 1 = D2 . ((1 + (indx D2,D1,i)) - 1) by A8, A10, JORDAN3:31
.= D1 . i by A1, A4, INTEGRA1:def 21 ;
j - i >= 0 by A3, XREAL_1:50;
then A13: (j - i) + 1 >= 0 + 1 by XREAL_1:8;
A14: ( 1 <= i & j <= len D1 ) by A1, A2, FINSEQ_3:27;
then A15: (mid D1,i,j) . 1 = D1 . ((1 + i) - 1) by A3, A13, JORDAN3:31
.= D1 . i ;
then consider C being closed-interval Subset of REAL such that
A16: ( r = lower_bound C & upper_bound C = (mid D1,i,j) . (len (mid D1,i,j)) & len (mid D1,i,j) = (j - i) + 1 & mid D1,i,j is Division of C ) by A1, A2, A3, A5, A12, Th11;
A17: (mid D1,i,j) . (len (mid D1,i,j)) = D1 . ((((j - i) + 1) - 1) + i) by A3, A13, A14, A16, JORDAN3:31
.= D1 . j ;
A18: MD2 . (len MD2) = D2 . (((((indx D2,D1,j) - (indx D2,D1,i)) + 1) - 1) + (indx D2,D1,i)) by A8, A9, A10, A11, JORDAN3:31
.= D1 . j by A2, A4, INTEGRA1:def 21 ;
A19: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:5
.= C by A9, A16, A17, A18, INTEGRA1:5 ;
then reconsider MD1 = mid D1,i,j as Division of B by A16, INTEGRA1:def 3;
A20: rng MD1 c= rng MD2

proof

A21: rng MD1 c= rng D1 by JORDAN3:28;
rng D1 c= rng D2 by A4, INTEGRA1:def 20;
then A22: rng MD1 c= rng D2 by A21, XBOOLE_1:1;
let x1 be set ; :: according to TARSKI:def 3 :: thesis:
assume A23: x1 in rng MD1 ; :: thesis:
then consider k2 being Element of NAT such that
A24: ( k2 in dom D2 & D2 . k2 = x1 ) by A22, PARTFUN1:26;
consider k1 being Element of NAT such that
A25: ( k1 in dom MD1 & MD1 . k1 = x1 ) by A23, PARTFUN1:26;
A26: ( 1 <= k1 & k1 <= len MD1 ) by A25, FINSEQ_3:27;
then 1 <= len MD1 by XXREAL_0:2;
then A27: 1 in dom MD1 by FINSEQ_3:27;
len MD1 in dom MD1 by FINSEQ_5:6;
then ( MD1 . 1 <= MD1 . k1 & MD1 . k1 <= MD1 . (len MD1) ) by A25, A26, A27, GOBOARD2:18;
then A28: ( indx D2,D1,i <= k2 & k2 <= indx D2,D1,j ) by A6, A7, A15, A17, A24, A25, SEQM_3:def 1;
then ( (indx D2,D1,i) + 1 <= k2 + 1 & k2 + 1 <= (indx D2,D1,j) + 1 ) by XREAL_1:8;
then A29: ( 1 <= (k2 + 1) - (indx D2,D1,i) & (k2 + 1) - (indx D2,D1,i) <= ((indx D2,D1,j) + 1) - (indx D2,D1,i) ) by XREAL_1:11, XREAL_1:21;
indx D2,D1,i <= k2 + 1 by A28, NAT_1:12;
then consider k3 being Nat such that
A30: k2 + 1 = (indx D2,D1,i) + k3 by NAT_1:10;
k3 in NAT by ORDINAL1:def 13;
then A31: MD2 . k3 = D2 . ((k3 + (indx D2,D1,i)) - 1) by A8, A11, A29, A30, JORDAN3:31;
k3 in dom MD2 by A9, A29, A30, FINSEQ_3:27;
hence x1 in rng MD2 by A24, A30, A31, FUNCT_1:def 5; :: thesis:

end;

len MD1 <= len MD2

proof

( MD1 is one-to-one & MD2 is one-to-one ) by JORDAN7:17;
then ( card (rng MD1) = len MD1 & card (rng MD2) = len MD2 ) by FINSEQ_4:77;
hence len MD1 <= len MD2 by A20, NAT_1:44; :: thesis:

end;

then MD1 <= MD2 by A20, INTEGRA1:def 20;
hence ex B being closed-interval Subset of REAL ex MD1, MD2 being Division of B st
( r = lower_bound B & upper_bound B = MD2 . (len MD2) & upper_bound B = MD1 . (len MD1) & MD1 <= MD2 & MD1 = mid D1,i,j & MD2 = mid D2,(indx D2,D1,i),(indx D2,D1,j) ) by A9, A16, A19; :: thesis: