for C being with_binary_products category
for a1, a2, b1, b2, c1, c2 being Object of C
for f1 being Morphism of a1,b1
for f2 being Morphism of a2,b2
for g1 being Morphism of b1,c1
for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)