theorem Th119: :: RELAT_1:127

for P, R being Relation holds rng (P * R) = R .: (rng P)