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