theorem :: FUNCT_3:34

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