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