rng f = dom g by FUNCT_2:def 3;
then dom (g * f) = dom f by RELAT_1:27;
hence g * f is with_cardinal_domain ; :: thesis: verum