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