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