:: deftheorem Def2 defines 'xor' IDEA_1:def 2 :
for n being Nat
for x, y, b₄ being Tuple of n, BOOLEAN holds
( b₄ = x 'xor' y iff for i being Nat st i in Seg n holds
b₄ /. i = (x /. i) 'xor' (y /. i) );