theorem Th27: :: BINARI_3:27

for n being non zero Nat
for k being Nat st k < 2 to_power n holds
(n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*>