dom f c= X ;
hence (id X) * f = f by RELAT_1:51; :: thesis: verum