theorem Th25: :: FUNCT_1:25

for f, g being Function st g * f is one-to-one & rng f c= dom g holds
f is one-to-one