theorem Th7: :: CAT_2:11

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