theorem Th28: :: BINARI_3:28

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