:: deftheorem Def20 defines ExtBit BINARI_6:def 4 :
for K being Nat
for x being Element of BOOLEAN * holds
( ( len x <= K implies ExtBit (x,K) = x ^ (0* (K -' (len x))) ) & ( not len x <= K implies ExtBit (x,K) = x | K ) );