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