theorem Th137: :: RELAT_1:147

for P, R being Relation holds dom (P * R) = P " (dom R)