for i being Nat holds (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>