let r be Real; :: thesis:
let i, j be Element of NAT ; :: thesis:
let A be non empty 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:25;
assume A3: j in dom D1 ; :: thesis:
assume A4: i <= j ; :: thesis:
then j - i >= 0 by XREAL_1:48;
then A5: (j - i) + 1 >= 0 + 1 by XREAL_1:6;
A6: j <= len D1 by A3, FINSEQ_3:25;
then A7: (mid (D1,i,j)) . 1 = D1 . ((1 + i) - 1) by A4, A5, A2, FINSEQ_6:122
.= D1 . i ;
assume A8: D1 <= D2 ; :: thesis:
then A9: D2 . (indx (D2,D1,i)) = D1 . i by A1, INTEGRA1:def 19;
A10: D2 . (indx (D2,D1,j)) = D1 . j by A3, A8, INTEGRA1:def 19;
A11: indx (D2,D1,i) in dom D2 by A1, A8, INTEGRA1:def 19;
then A12: 1 <= indx (D2,D1,i) by FINSEQ_3:25;
A13: indx (D2,D1,j) in dom D2 by A3, A8, INTEGRA1:def 19;
then A14: indx (D2,D1,j) <= len D2 by FINSEQ_3:25;
D1 . i <= D1 . j by A1, A3, A4, SEQ_4:137;
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 non empty 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
A19: mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) is Division of B by A11, A13, A15, Th12;
A20: 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:58;
reconsider MD2 = mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j))) as Division of B by A19;
(indx (D2,D1,j)) - (indx (D2,D1,i)) >= 0 by A15, XREAL_1:48;
then A21: ((indx (D2,D1,j)) - (indx (D2,D1,i))) + 1 >= 0 + 1 by XREAL_1:6;
then A22: MD2 . (len MD2) = D2 . (((((indx (D2,D1,j)) - (indx (D2,D1,i))) + 1) - 1) + (indx (D2,D1,i))) by A15, A20, A12, A14, FINSEQ_6:122
.= D1 . j by A3, A8, INTEGRA1:def 19 ;
MD2 . 1 = D2 . ((1 + (indx (D2,D1,i))) - 1) by A15, A21, A12, A14, FINSEQ_6:122
.= D1 . i by A1, A8, INTEGRA1:def 19 ;
then consider C being non empty 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
A25: mid (D1,i,j) is Division of C by A1, A3, A4, A16, A7, Th12;
len (mid (D1,i,j)) = (j - i) + 1 by A1, A3, A4, INTEGRA1:58;
then A26: (mid (D1,i,j)) . (len (mid (D1,i,j))) = D1 . ((((j - i) + 1) - 1) + i) by A4, A5, A2, A6, FINSEQ_6:122
.= D1 . j ;
A27: B = [.(lower_bound B),(upper_bound B).] by INTEGRA1:4
.= C by A17, A18, A23, A24, A26, A22, INTEGRA1:4 ;
then reconsider MD1 = mid (D1,i,j) as Division of B by A25;
A28: rng MD1 c= rng MD2

proof

let x1 be object ; :: according to TARSKI:def 3 :: thesis:
A29: rng MD1 c= rng D1 by FINSEQ_6:119;
assume A30: x1 in rng MD1 ; :: thesis:
then consider k1 being Element of NAT such that
A31: k1 in dom MD1 and
A32: MD1 . k1 = x1 by PARTFUN1:3;
rng D1 c= rng D2 by A8, INTEGRA1:def 18;
then rng MD1 c= rng D2 by A29;
then consider k2 being Element of NAT such that
A33: k2 in dom D2 and
A34: D2 . k2 = x1 by A30, PARTFUN1:3;
A35: k1 <= len MD1 by A31, FINSEQ_3:25;
A36: 1 <= k1 by A31, FINSEQ_3:25;
then 1 <= len MD1 by A35, XXREAL_0:2;
then 1 in dom MD1 by FINSEQ_3:25;
then MD1 . 1 <= MD1 . k1 by A31, A36, SEQ_4:137;
then A37: indx (D2,D1,i) <= k2 by A11, A9, A7, A33, A34, A32, SEQM_3:def 1;
then consider k3 being Nat such that
A38: 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 A31, A35, SEQ_4:137;
then k2 <= indx (D2,D1,j) by A13, A10, A26, A33, A34, A32, SEQM_3:def 1;
then k2 + 1 <= (indx (D2,D1,j)) + 1 by XREAL_1:6;
then A39: (k2 + 1) - (indx (D2,D1,i)) <= ((indx (D2,D1,j)) + 1) - (indx (D2,D1,i)) by XREAL_1:9;
(indx (D2,D1,i)) + 1 <= k2 + 1 by A37, XREAL_1:6;
then A40: 1 <= (k2 + 1) - (indx (D2,D1,i)) by XREAL_1:19;
then A41: k3 in dom MD2 by A20, A39, A38, FINSEQ_3:25;
MD2 . k3 = D2 . ((k3 + (indx (D2,D1,i))) - 1) by A15, A12, A14, A40, A39, A38, FINSEQ_6:122;
hence x1 in rng MD2 by A34, A38, A41, FUNCT_1:def 3; :: thesis:

end;

A42: card (rng MD2) = len MD2 by FINSEQ_4:62;
card (rng MD1) = len MD1 by FINSEQ_4:62;
then len MD1 <= len MD2 by A28, A42, NAT_1:43;
then MD1 <= MD2 by A28, INTEGRA1:def 18;
hence ex B being non empty 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, A27; :: thesis: