let i, j be Element of NAT ; :: thesis: for A being 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 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 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 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 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 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:3;
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 2;
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:3;
then j - (i -' 1) = j - (i - 1) by XREAL_1:235;
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:3;
then j - (i -' 1) <= (len D) - (i -' 1) by XREAL_1:11;
then A6: (j -' i) + 1 <= len (D /^ (i -' 1)) by A3, A4, A5, XREAL_1:235;
A7: mid (D,i,j) = (D /^ (i -' 1)) | ((j -' i) + 1) by A3, FINSEQ_6:def 3
.= D1 | (Seg k) by FINSEQ_1:def 15 ;
then 0 < len (mid (D,i,j)) by A6, FINSEQ_1:21;
then reconsider M = mid (D,i,j) as non empty increasing FinSequence of REAL by A2, A3, Th37;
(j -' i) + 1 >= 0 + 1 by XREAL_1:8;
then A9: 1 <= len M by A6, A7, FINSEQ_1:21;
then len M in Seg (len M) by FINSEQ_1:3;
then A10: len M in dom M by FINSEQ_1:def 3;
1 in Seg (len M) by A9, FINSEQ_1:3;
then A11: 1 in dom M by FINSEQ_1:def 3;
then M . 1 <= M . (len M) by A9, A10, SEQ_4:154;
then reconsider B = [.(M . 1),(M . (len M)).] as closed-interval Subset of REAL by Def1;
A12: B = [.(lower_bound B),(upper_bound B).] by Th5;
then A13: lower_bound B = M . 1 by Th6;
A14: M . (len M) = upper_bound B by A12, Th6;
for x being Real st x in rng M holds
x in B

proof

let x be 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
A15: i in dom M and
A16: x = M . i by PARTFUN1:26;
A17: i in Seg (len M) by A15, FINSEQ_1:def 3;
then i <= len M by FINSEQ_1:3;
then A18: M . i <= M . (len M) by A10, A15, SEQ_4:154;
1 <= i by A17, FINSEQ_1:3;
then M . 1 <= M . i by A11, A15, SEQ_4:154;
then M . i in { a where a is Real : ( M . 1 <= a & a <= M . (len M) ) } by A18;
hence x in B by A16, RCOMP_1:def 1; :: thesis: verum

end;

then rng M c= B by SUBSET_1:7;
then M is Division of B by A14, Def2;
hence ex B being 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 A13, A14; :: thesis: verum