let A be non empty closed_interval Subset of REAL; for n being Nat st vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 holds
divset ((EqDiv (A,(2 |^ n))),1) = A
let n be Nat; ( vol A > 0 & len (EqDiv (A,(2 |^ n))) = 1 implies divset ((EqDiv (A,(2 |^ n))),1) = A )
assume that
A1:
vol A > 0
and
A2:
len (EqDiv (A,(2 |^ n))) = 1
; divset ((EqDiv (A,(2 |^ n))),1) = A
2 |^ n > 0
by NEWTON:83;
then A3:
EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n
by A1, Def1;
A4:
1 in dom (EqDiv (A,(2 |^ n)))
by A2, FINSEQ_3:25;
then
( lower_bound (divset ((EqDiv (A,(2 |^ n))),1)) = lower_bound A & upper_bound (divset ((EqDiv (A,(2 |^ n))),1)) = (EqDiv (A,(2 |^ n))) . 1 )
by INTEGRA1:def 4;
then A5:
divset ((EqDiv (A,(2 |^ n))),1) = [.(lower_bound A),((EqDiv (A,(2 |^ n))) . 1).]
by INTEGRA1:4;
(EqDiv (A,(2 |^ n))) . 1 = (lower_bound A) + (((vol A) / 1) * 1)
by A2, A3, A4, INTEGRA4:def 1;
then
(EqDiv (A,(2 |^ n))) . 1 = (lower_bound A) + ((upper_bound A) - (lower_bound A))
by INTEGRA1:def 5;
hence
divset ((EqDiv (A,(2 |^ n))),1) = A
by A5, INTEGRA1:4; verum