theorem Th19: :: RELAT_1:25

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