( x in I or x nin dom X ) ;
hence X . x is countable by Def1, FUNCT_1:def 2; :: thesis: verum