A5: rng (p '&' q) c= BOOLEAN by Def16;
( dom p = A & dom q = A ) by PARTFUN1:def 2;
then dom (p '&' q) = A /\ A by Def18
.= A ;
hence p '&' q is Function of A,BOOLEAN by A5, FUNCT_2:2; :: thesis: verum