:: deftheorem Def5 defines + BINARITH:def 5 :
for n being non zero Nat
for x, y, b₄ being Tuple of n, BOOLEAN holds
( b₄ = x + y iff for i being Nat st i in Seg n holds
b₄ /. i = ((x /. i) 'xor' (y /. i)) 'xor' ((carry (x,y)) /. i) );