let A be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum