let i, j be Element of NAT ; :: thesis: for A, B 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 & D . i >= lower_bound B & D . j = upper_bound B holds
mid (D,i,j) is Division of B
let A, B 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 & D . i >= lower_bound B & D . j = upper_bound B holds
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 & D . i >= lower_bound B & D . j = upper_bound B implies 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 and
A4: D . i >= lower_bound B and
A5: D . j = upper_bound B ; :: thesis: mid (D,i,j) is Division of B
A6: (((j - i) + 1) + i) - 1 = j ;
i in Seg (len D) by A1, FINSEQ_1:def 3;
then A7: 1 <= i by FINSEQ_1:1;
0 <= j - i by A3, XREAL_1:48;
then A8: 0 + 1 <= (j - i) + 1 by XREAL_1:6;
j in Seg (len D) by A2, FINSEQ_1:def 3;
then A9: j <= len D by FINSEQ_1:1;
consider A1 being non empty closed_interval Subset of REAL such that
A10: lower_bound A1 = (mid (D,i,j)) . 1 and
A11: upper_bound A1 = (mid (D,i,j)) . (len (mid (D,i,j))) and
A12: mid (D,i,j) is Division of A1 by A1, A2, A3, Th34;
A13: len (mid (D,i,j)) = (j - i) + 1 by A1, A2, A3, Lm1;
A14: (1 + i) - 1 = i ;
for x being Element of REAL st x in A1 holds
x in B

proof

let x be Element of REAL ; :: thesis: ( x in A1 implies x in B )
assume x in A1 ; :: thesis: x in B
then x in [.(lower_bound A1),(upper_bound A1).] by Th2;
then x in { a where a is Real : ( lower_bound A1 <= a & a <= upper_bound A1 ) } by RCOMP_1:def 1;
then A15: ex a being Real st
( x = a & lower_bound A1 <= a & a <= upper_bound A1 ) ;
then D . i <= x by A3, A10, A7, A9, A8, A14, FINSEQ_6:122;
then A16: lower_bound B <= x by A4, XXREAL_0:2;
x <= upper_bound B by A3, A5, A11, A13, A7, A9, A8, A6, A15, FINSEQ_6:122;
then x in { a where a is Real : ( lower_bound B <= a & a <= upper_bound B ) } by A16;
then x in [.(lower_bound B),(upper_bound B).] by RCOMP_1:def 1;
hence x in B by Th2; :: thesis: verum

end;

then A17: A1 c= B ;
rng (mid (D,i,j)) c= A1 by A12, Def1;
then A18: rng (mid (D,i,j)) c= B by A17;
(mid (D,i,j)) . (len (mid (D,i,j))) = D . j by A3, A13, A7, A9, A8, A6, FINSEQ_6:122;
hence mid (D,i,j) is Division of B by A5, A12, A18, Def1; :: thesis: verum