let r be Real; :: thesis: for i, j being Element of NAT

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

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

let i, j be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

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

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

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

let D1, D2 be Division of A; :: thesis: ( i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 implies 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))) ) )

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: ( not j in dom D1 or not i <= j or not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

then A2: 1 <= i by FINSEQ_3:25;

assume A3: j in dom D1 ; :: thesis: ( not i <= j or not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

assume A4: i <= j ; :: thesis: ( not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

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: ( not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

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

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

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: verum

for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

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

let i, j be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

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

let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A st i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 holds

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

let D1, D2 be Division of A; :: thesis: ( i in dom D1 & j in dom D1 & i <= j & D1 <= D2 & r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 implies 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))) ) )

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: ( not j in dom D1 or not i <= j or not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

then A2: 1 <= i by FINSEQ_3:25;

assume A3: j in dom D1 ; :: thesis: ( not i <= j or not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

assume A4: i <= j ; :: thesis: ( not D1 <= D2 or not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

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: ( not r < (mid (D2,(indx (D2,D1,i)),(indx (D2,D1,j)))) . 1 or 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))) ) )

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

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

A42:
card (rng MD2) = len MD2
by FINSEQ_4:62;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng MD1 or x1 in rng MD2 )

A29: rng MD1 c= rng D1 by FINSEQ_6:119;

assume A30: x1 in rng MD1 ; :: thesis: x1 in rng MD2

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: verum

end;A29: rng MD1 c= rng D1 by FINSEQ_6:119;

assume A30: x1 in rng MD1 ; :: thesis: x1 in rng MD2

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: verum

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: verum