( dom p = A & dom q = A ) by PARTFUN1:def 2;
then A6: dom (p 'xor' q) = A /\ A by Def3
.= A ;
rng (p 'xor' q) c= BOOLEAN by MARGREL1:def 16;
hence p 'xor' q is Function of A,BOOLEAN by A6, FUNCT_2:2; :: thesis: verum