theorem :: NTALGO_2:12

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