theorem Th4: :: FUNCT_3:4

for Y being set
for f, g being Function st Y c= rng (g * f) & g is one-to-one holds
g " Y c= rng f