:: deftheorem Def4 defines Op-XOR DESCIP_1:def 4 :
for n being non zero Element of NAT
for s, t, b₄ being Element of n -tuples_on BOOLEAN holds
( b₄ = Op-XOR (s,t) iff for i being Nat st i in Seg n holds
b₄ . i = (s . i) 'xor' (t . i) );