let i, j be Element of NAT ; :: thesis: for A, B being 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 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:3;
0 <= j - i by A3, XREAL_1:50;
then A8: 0 + 1 <= (j - i) + 1 by XREAL_1:8;
j in Seg (len D) by A2, FINSEQ_1:def 3;
then A9: j <= len D by FINSEQ_1:3;
consider A1 being 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
A13: mid (D,i,j) is Division of A1 by A1, A2, A3, Th38;
A12: len (mid (D,i,j)) = (j - i) + 1 by A1, A2, A3, Th38a;
A14: (1 + i) - 1 = i ;
for x being Real st x in A1 holds
x in B

proof

let x be 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 Th5;
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:128;
then A16: lower_bound B <= x by A4, XXREAL_0:2;
x <= upper_bound B by A3, A5, A11, A12, A7, A9, A8, A6, A15, FINSEQ_6:128;
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 Th5; :: thesis: verum

end;

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