ex f being Function st
( p = f & dom f = A & rng f c= BOOLEAN ) by FUNCT_2:def 2;
then A1: dom ('not' p) = A by Def18;
rng ('not' p) c= BOOLEAN by Def17;
hence 'not' p is Element of Funcs (A,BOOLEAN) by A1, FUNCT_2:def 2; :: thesis: verum