theorem Th47: :: RELAT_1:53

for Y being set
for R being Relation st rng R c= Y holds
R * (id Y) = R