theorem Th26: :: BINARI_3:26

for n, k being Nat st k < 2 to_power n holds
((n + 1) -BinarySequence k) . (n + 1) = FALSE