theorem LMExtBit1: :: BINARI_6:13

for K being Nat
for x being Element of BOOLEAN * st len x <= K holds
ExtBit (x,(K + 1)) = (ExtBit (x,K)) ^ <*0*>