let i, j be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D & j in dom D & i <= j holds
ex B being non empty closed_interval Subset of REAL st
( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )
let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A st i in dom D & j in dom D & i <= j holds
ex B being non empty closed_interval Subset of REAL st
( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )
let D be Division of A; :: thesis: ( i in dom D & j in dom D & i <= j implies ex B being non empty closed_interval Subset of REAL st
( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) )
assume that
A1: i in dom D and
A2: j in dom D and
A3: i <= j ; :: thesis: ex B being non empty closed_interval Subset of REAL st
( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B )
j in Seg (len D) by A2, FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then i <= len D by A3, XXREAL_0:2;
then i -' 1 <= len D by NAT_D:44;
then A4: len (D /^ (i -' 1)) = (len D) - (i -' 1) by RFINSEQ:def 1;
reconsider D1 = D /^ (i -' 1) as FinSequence of REAL ;
reconsider k = (j -' i) + 1 as Element of NAT ;
i in Seg (len D) by A1, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then j - (i -' 1) = j - (i - 1) by XREAL_1:233;
then A5: j - (i -' 1) = (j - i) + 1 ;
j in Seg (len D) by A2, FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:1;
then j - (i -' 1) <= (len D) - (i -' 1) by XREAL_1:9;
then A6: (j -' i) + 1 <= len (D /^ (i -' 1)) by A3, A4, A5, XREAL_1:233;
A7: mid (D,i,j) = (D /^ (i -' 1)) | ((j -' i) + 1) by A3, FINSEQ_6:def 3
.= D1 | (Seg k) by FINSEQ_1:def 16 ;
then 0 < len (mid (D,i,j)) by A6, FINSEQ_1:17;
then reconsider M = mid (D,i,j) as non empty increasing FinSequence of REAL by A2, A3, Th33;
(j -' i) + 1 >= 0 + 1 by XREAL_1:6;
then A8: 1 <= len M by A6, A7, FINSEQ_1:17;
then len M in Seg (len M) by FINSEQ_1:1;
then A9: len M in dom M by FINSEQ_1:def 3;
1 in Seg (len M) by A8, FINSEQ_1:1;
then A10: 1 in dom M by FINSEQ_1:def 3;
then M . 1 <= M . (len M) by A8, A9, SEQ_4:137;
then reconsider B = [.(M . 1),(M . (len M)).] as non empty closed_interval Subset of REAL by MEASURE5:14;
A11: B = [.(lower_bound B),(upper_bound B).] by Th2;
then A12: lower_bound B = M . 1 by Th3;
A13: M . (len M) = upper_bound B by A11, Th3;
for x being Element of REAL st x in rng M holds
x in B

proof

let x be Element of REAL ; :: thesis: ( x in rng M implies x in B )
assume x in rng M ; :: thesis: x in B
then consider i being Element of NAT such that
A14: i in dom M and
A15: x = M . i by PARTFUN1:3;
A16: i in Seg (len M) by A14, FINSEQ_1:def 3;
then i <= len M by FINSEQ_1:1;
then A17: M . i <= M . (len M) by A9, A14, SEQ_4:137;
1 <= i by A16, FINSEQ_1:1;
then M . 1 <= M . i by A10, A14, SEQ_4:137;
then M . i in { a where a is Real : ( M . 1 <= a & a <= M . (len M) ) } by A17;
hence x in B by A15, RCOMP_1:def 1; :: thesis: verum

end;

then rng M c= B ;
then M is Division of B by A13, Def1;
hence ex B being non empty closed_interval Subset of REAL st
( lower_bound B = (mid (D,i,j)) . 1 & upper_bound B = (mid (D,i,j)) . (len (mid (D,i,j))) & mid (D,i,j) is Division of B ) by A12, A13; :: thesis: verum