A1: 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 A2: dom (p 'nand' q) = A /\ A by A1, Def1
.= A ;
rng (p 'nand' q) c= BOOLEAN by MARGREL1:def 17;
hence p 'nand' q is Element of Funcs A,BOOLEAN by A2, FUNCT_2:def 2; :: thesis: verum