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