Coim (f,a) is Subset of X ;
hence eq_dom (f,a) is Subset of X ; :: thesis: verum