for P, R being Relation st rng R c= dom P holds
dom (R * P) = dom R