theorem :: RELAT_1:103

for X, Y being set
for R being Relation holds (X \/ Y) |` R = (X |` R) \/ (Y |` R)