theorem LMExtBit3: :: BINARI_6:18

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