theorem Th24: :: CAT_2:30

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