theorem :: CAT_1:17

for C being Category
for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Def5;