theorem Th66:
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)