for K being non zero Nat
for x, y being Tuple of K, BOOLEAN st y = 0* K holds
( x + y = x & y + x = x )