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