theorem :: FUNCT_3:18

for f, g being Function holds .: (g * f) = (.: g) * (.: f)