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 S₁[ 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 S₁[n,D]

proof

let n be Element of NAT ; :: thesis: ex D being Element of divs A st S₁[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 S₁[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 S₁[n,D . n] from FUNCT_2:sch 3(A3);
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

let n be Nat; :: thesis: D . n divide_into_equal 2 |^ n
n is Element of NAT by ORDINAL1:def 12;
then ex d being Division of A st
( d = D . n & d divide_into_equal 2 |^ n ) by A5;
hence D . n divide_into_equal 2 |^ n ; :: thesis: verum

end;