for K being non zero Nat
for x being Element of BOOLEAN * st len x = K holds
ExtBit (x,K) = x