A5: rng (p '&' q) c= BOOLEAN by Def17;
A6: ex f being Function st
( q = f & dom f = A & rng f c= BOOLEAN ) by FUNCT_2:def 2;
ex f being Function st
( p = f & dom f = A & rng f c= BOOLEAN ) by FUNCT_2:def 2;
then dom (p '&' q) = A /\ A by A6, Def19
.= A ;
hence p '&' q is Element of Funcs (A,BOOLEAN) by A5, FUNCT_2:def 2; :: thesis: verum