theorem Th24: :: FUNCT_1:24

for f, g being Function st f is one-to-one & g is one-to-one holds
g * f is one-to-one