for C being Category
for a being Object of C
for f, g being Morphism of C st dom g = cod f holds
hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))