theorem :: FUNCT_1:44

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