theorem Th55: :: ENS_1:56

for C being Category
for f, g, f9, g9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds
hom ((f (*) g),(g9 (*) f9)) = (hom (g,g9)) * (hom (f,f9))