theorem :: RELAT_1:52

for R being Relation holds (id (dom R)) * R = R by Th45;