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:
set MD1 = mid D1,i,j;
set MD2 = mid D2,(indx D2,D1,i),(indx D2,D1,j);
assume A1: i in dom D1 ; :: thesis:
then A2: 1 <= i by FINSEQ_3:27;
assume A3: j in dom D1 ; :: thesis:
assume A4: i <= j ; :: thesis:
then j - i >= 0 by XREAL_1:50;
then A5: (j - i) + 1 >= 0 + 1 by XREAL_1:8;
A6: j <= len D1 by A3, FINSEQ_3:27;
then A7: (mid D1,i,j) . 1 = D1 . ((1 + i) - 1) by A4, A5, A2, FINSEQ_6:128
.= D1 . i ;
assume A8: D1 <= D2 ; :: thesis:
then A9: D2 . (indx D2,D1,i) = D1 . i by A1, INTEGRA1:def 21;
A10: D2 . (indx D2,D1,j) = D1 . j by A3, A8, INTEGRA1:def 21;
A11: indx D2,D1,i in dom D2 by A1, A8, INTEGRA1:def 21;
then A12: 1 <= indx D2,D1,i by FINSEQ_3:27;
A13: indx D2,D1,j in dom D2 by A3, A8, INTEGRA1:def 21;
then A14: indx D2,D1,j <= len D2 by FINSEQ_3:27;
D1 . i <= D1 . j by A1, A3, A4, SEQ_4:154;
then A15: indx D2,D1,i <= indx D2,D1,j by A11, A9, A13, A10, SEQM_3:def 1;
assume A16: r < (mid D2,(indx D2,D1,i),(indx D2,D1,j)) . 1 ; :: thesis:
then consider B being closed-interval Subset of REAL such that
A17: r = lower_bound B and
A18: upper_bound B = (mid D2,(indx D2,D1,i),(indx D2,D1,j)) . (len (mid D2,(indx D2,D1,i),(indx D2,D1,j))) and
A20: mid D2,(indx D2,D1,i),(indx D2,D1,j) is Division of B by A11, A13, A15, Th11;
A19: len (mid D2,(indx D2,D1,i),(indx D2,D1,j)) = ((indx D2,D1,j) - (indx D2,D1,i)) + 1 by A11, A13, A15, INTEGRA1:60;
reconsider MD2 = mid D2,(indx D2,D1,i),(indx D2,D1,j) as Division of B by A20;
(indx D2,D1,j) - (indx D2,D1,i) >= 0 by A15, XREAL_1:50;
then A21: ((indx D2,D1,j) - (indx D2,D1,i)) + 1 >= 0 + 1 by XREAL_1:8;
then A22: MD2 . (len MD2) = D2 . (((((indx D2,D1,j) - (indx D2,D1,i)) + 1) - 1) + (indx D2,D1,i)) by A15, A19, A12, A14, FINSEQ_6:128
.= D1 . j by A3, A8, INTEGRA1:def 21 ;
MD2 . 1 = D2 . ((1 + (indx D2,D1,i)) - 1) by A15, A21, A12, A14, FINSEQ_6:128
.= D1 . i by A1, A8, INTEGRA1:def 21 ;
then consider C being closed-interval Subset of REAL such that
A23: r = lower_bound C and
A24: upper_bound C = (mid D1,i,j) . (len (mid D1,i,j)) and
A26: mid D1,i,j is Division of C by A1, A3, A4, A16, A7, Th11;
len (mid D1,i,j) = (j - i) + 1 by A1, A3, A4, INTEGRA1:60;
then A27: (mid D1,i,j) . (len (mid D1,i,j)) = D1 . ((((j - i) + 1) - 1) + i) by A4, A5, A2, A6, FINSEQ_6:128
.= D1 . j ;
A28: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:5
.= C by A17, A18, A23, A24, A27, A22, INTEGRA1:5 ;
then reconsider MD1 = mid D1,i,j as Division of B by A26;
A29: rng MD1 c= rng MD2

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis:
A30: rng MD1 c= rng D1 by FINSEQ_6:125;
assume A31: x1 in rng MD1 ; :: thesis:
then consider k1 being Element of NAT such that
A32: k1 in dom MD1 and
A33: MD1 . k1 = x1 by PARTFUN1:26;
rng D1 c= rng D2 by A8, INTEGRA1:def 20;
then rng MD1 c= rng D2 by A30, XBOOLE_1:1;
then consider k2 being Element of NAT such that
A34: k2 in dom D2 and
A35: D2 . k2 = x1 by A31, PARTFUN1:26;
A36: k1 <= len MD1 by A32, FINSEQ_3:27;
A37: 1 <= k1 by A32, FINSEQ_3:27;
then 1 <= len MD1 by A36, XXREAL_0:2;
then 1 in dom MD1 by FINSEQ_3:27;
then MD1 . 1 <= MD1 . k1 by A32, A37, SEQ_4:154;
then A38: indx D2,D1,i <= k2 by A11, A9, A7, A34, A35, A33, SEQM_3:def 1;
then consider k3 being Nat such that
A39: k2 + 1 = (indx D2,D1,i) + k3 by NAT_1:10, NAT_1:12;
len MD1 in dom MD1 by FINSEQ_5:6;
then MD1 . k1 <= MD1 . (len MD1) by A32, A36, SEQ_4:154;
then k2 <= indx D2,D1,j by A13, A10, A27, A34, A35, A33, SEQM_3:def 1;
then k2 + 1 <= (indx D2,D1,j) + 1 by XREAL_1:8;
then A40: (k2 + 1) - (indx D2,D1,i) <= ((indx D2,D1,j) + 1) - (indx D2,D1,i) by XREAL_1:11;
(indx D2,D1,i) + 1 <= k2 + 1 by A38, XREAL_1:8;
then A41: 1 <= (k2 + 1) - (indx D2,D1,i) by XREAL_1:21;
then A42: k3 in dom MD2 by A19, A40, A39, FINSEQ_3:27;
k3 in NAT by ORDINAL1:def 13;
then MD2 . k3 = D2 . ((k3 + (indx D2,D1,i)) - 1) by A15, A12, A14, A41, A40, A39, FINSEQ_6:128;
hence x1 in rng MD2 by A35, A39, A42, FUNCT_1:def 5; :: thesis:

end;

A43: card (rng MD2) = len MD2 by FINSEQ_4:77;
card (rng MD1) = len MD1 by FINSEQ_4:77;
then len MD1 <= len MD2 by A29, A43, NAT_1:44;
then MD1 <= MD2 by A29, 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 A17, A18, A24, A28; :: thesis: