( x in dom f or not x in dom f ) ;
hence f . x is empty by Def2, Def8; :: thesis: verum