( a in dom f or not a in dom f ) ;
hence not f . a is negative by FUNCT_1:def 2; :: thesis: verum