theorem :: RELAT_1:108

for Y being set
for P, R being Relation holds Y |` (P * R) = P * (Y |` R)