theorem Th23: :: CAT_2:29

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