:: deftheorem Def3 defines 'xor' BVFUNC_1:def 3 :
for p, q being boolean-valued Function
for b₃ being Function holds
( b₃ = p 'xor' q iff ( dom b₃ = (dom p) /\ (dom q) & ( for x being set st x in dom b₃ holds
b₃ . x = (p . x) 'xor' (q . x) ) ) );