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