:: deftheorem Def1 defines XORB NBVECTSP:def 1 :
for n being non zero Element of NAT
for b₂ being BinOp of (n -tuples_on BOOLEAN) holds
( b₂ = XORB n iff for x, y being Element of n -tuples_on BOOLEAN holds b₂ . (x,y) = Op-XOR (x,y) );