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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & 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)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of B )
i -' 1 <= len D

proof

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;
hence i -' 1 <= len D by NAT_D:44; :: thesis: verum

end;

then A4: len (D /^ (i -' 1)) = (len D) - (i -' 1) by RFINSEQ:def 2;
A5: (j -' i) + 1 <= len (D /^ (i -' 1))

proof

j in Seg (len D) by A2, FINSEQ_1:def 3;
then j <= len D by FINSEQ_1:3;
then A6: j - (i -' 1) <= (len D) - (i -' 1) by XREAL_1:11;
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 j - (i -' 1) = (j - i) + 1 ;
hence (j -' i) + 1 <= len (D /^ (i -' 1)) by A3, A4, A6, XREAL_1:235; :: thesis: verum

end;

reconsider k = (j -' i) + 1 as Element of NAT ;
reconsider D1 = D /^ (i -' 1) as FinSequence of REAL ;
reconsider D2 = D1 | (Seg k) as FinSequence of REAL by FINSEQ_1:23;
A7: mid D,i,j = D2

proof

mid D,i,j = (D /^ (i -' 1)) | ((j -' i) + 1) by A3, JORDAN3:def 1
.= D1 | (Seg k) by FINSEQ_1:def 15 ;
hence mid D,i,j = D2 ; :: thesis: verum

end;

then A8: len (mid D,i,j) = (j -' i) + 1 by A5, FINSEQ_1:21;
0 < len (mid D,i,j) by A5, A7, FINSEQ_1:21;
then reconsider M = mid D,i,j as non empty increasing FinSequence of REAL by A2, A3, Th37;
A9: 1 <= len M

proof

(j -' i) + 1 >= 0 + 1 by XREAL_1:8;
hence 1 <= len M by A5, A7, FINSEQ_1:21; :: thesis: verum

end;

A10: ( 1 in dom M & len M in dom M )

proof

1 in Seg (len M) by A9, FINSEQ_1:3;
hence 1 in dom M by FINSEQ_1:def 3; :: thesis: len M in dom M
len M in Seg (len M) by A9, FINSEQ_1:3;
hence len M in dom M by FINSEQ_1:def 3; :: thesis: verum

end;

then M . 1 <= M . (len M) by A9, GOBOARD2:18;
then reconsider B = [.(M . 1),(M . (len M)).] as closed-interval Subset of REAL by Def1;
A11: rng M c= B

proof

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
A12: ( i in dom M & x = M . i ) by PARTFUN1:26;
i in Seg (len M) by A12, FINSEQ_1:def 3;
then ( 1 <= i & i <= len M ) by FINSEQ_1:3;
then ( M . 1 <= M . i & M . i <= M . (len M) ) by A10, A12, GOBOARD2:18;
then M . i in { a where a is Real : ( M . 1 <= a & a <= M . (len M) ) } ;
hence x in B by A12, RCOMP_1:def 1; :: thesis: verum

end;

hence rng M c= B by SUBSET_1:7; :: thesis: verum

end;

A13: len (mid D,i,j) = (j - i) + 1 by A3, A8, XREAL_1:235;
A14: B = [.(lower_bound B),(upper_bound B).] by Th5;
then A15: lower_bound B = M . 1 by Th6;
A16: M . (len M) = upper_bound B by A14, Th6;
then M is Division of B by A11, 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)) & len (mid D,i,j) = (j - i) + 1 & mid D,i,j is Division of B ) by A13, A15, A16; :: thesis: verum