Coim (f,x) c= dom f by RELAT_1:132;
hence Coim (f,x) is finite ; :: thesis: verum