theorem Th55: :: RELAT_1:61

for X being set
for R being Relation holds dom (R | X) = (dom R) /\ X