( x in dom f or not x in dom f ) ;
hence f . x is empty by FUNCT_1:def 4, FUNCT_1:def 14; :: thesis: verum