for X being set
for P, R being Relation holds P * (R | X) = (X |` P) * R by Lm36;