theorem Th87: :: RELAT_1:93

for Y being set
for R being Relation holds Y |` R = R /\ [:(dom R),Y:]