dom P = rng R by PARTFUN1:def 2;
then dom (R * P) = dom R by RELAT_1:27;
hence R * P is with_cardinal_domain ; :: thesis: verum