theorem LMExtBit4: :: BINARI_6:16

for K being non zero Nat
for y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
y /. n = 0