let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL st a < b & A = [.a,b.] holds
ex D being DivSequence of A st
for n being Nat holds D . n divide_into_equal 2 |^ n

let A be non empty closed_interval Subset of REAL; :: thesis: ( a < b & A = [.a,b.] implies ex D being DivSequence of A st
for n being Nat holds D . n divide_into_equal 2 |^ n )

assume that
A1: a < b and
A2: A = [.a,b.] ; :: thesis: ex D being DivSequence of A st
for n being Nat holds D . n divide_into_equal 2 |^ n

defpred S1[ Nat, object ] means ex D being Division of A st
( D = \$2 & D divide_into_equal 2 |^ \$1 );
A3: for n being Element of NAT ex D being Element of divs A st S1[n,D]
proof
let n be Element of NAT ; :: thesis: ex D being Element of divs A st S1[n,D]
2 |^ n > 0 by NEWTON:83;
then consider D1 being Division of A such that
A4: D1 divide_into_equal 2 |^ n by A1, A2, Th8;
D1 is Element of divs A by INTEGRA1:def 3;
hence ex D being Element of divs A st S1[n,D] by A4; :: thesis: verum
end;
consider D being Function of NAT,(divs A) such that
A5: for n being Element of NAT holds S1[n,D . n] from reconsider D = D as DivSequence of A ;
take D ; :: thesis: for n being Nat holds D . n divide_into_equal 2 |^ n
thus for n being Nat holds D . n divide_into_equal 2 |^ n :: thesis: verum
proof end;