for n being Nat holds Nat2BL . (2 |^ n) = (0* n) ^ <*1*>