consider i being Element of NAT such that
i <= 2 |^ n and
A1: x = i / (2 |^ n) by Def3;
take i ; :: thesis: x = i / (2 |^ n)
thus x = i / (2 |^ n) by A1; :: thesis: verum