let n be Nat; :: thesis: for x being Element of dyadic n holds

( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )

let x be Element of dyadic n; :: thesis: ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )

ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) by Def1;

hence ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) by Def5; :: thesis: verum

( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )

let x be Element of dyadic n; :: thesis: ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n )

ex i being Nat st

( i <= 2 |^ n & x = i / (2 |^ n) ) by Def1;

hence ( x = (axis x) / (2 |^ n) & axis x <= 2 |^ n ) by Def5; :: thesis: verum