A17: Coim f,a is Subset of X ;
thus eq_dom f,a is Subset of X by A17; :: thesis: verum