f " x c= dom f by RELAT_1:132;
hence f " x is finite ; :: thesis: verum