theorem LMExtBit501: :: BINARI_6:17

for K being non zero Nat
for x, y being Tuple of K, BOOLEAN holds carry (x,y) = carry (y,x)