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_{1}[ 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_{1}[n,D]

A5: for n being Element of NAT holds S_{1}[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

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

( D = $2 & D divide_into_equal 2 |^ $1 );

A3: for n being Element of NAT ex D being Element of divs A st S

proof

consider D being Function of NAT,(divs A) such that
let n be Element of NAT ; :: thesis: ex D being Element of divs A st S_{1}[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_{1}[n,D]
by A4; :: thesis: verum

end;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

A5: for n being Element of NAT holds S

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;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