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