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