theorem :: RELAT_1:54

for R being Relation holds R * (id (rng R)) = R by Th47;