A1: dom ('not' p) = dom p by Def17
.= A by PARTFUN1:def 2 ;
rng ('not' p) c= BOOLEAN by Def16;
hence 'not' p is Function of A,BOOLEAN by A1, FUNCT_2:2; :: thesis: verum