theorem Th11:
for
A,
B being non
empty transitive AltCatStr holds
(
A,
B have_the_same_composition iff for
a1,
a2,
a3 being
Object of
A st
<^a1,a2^> <> {} &
<^a2,a3^> <> {} holds
for
b1,
b2,
b3 being
Object of
B st
<^b1,b2^> <> {} &
<^b2,b3^> <> {} &
b1 = a1 &
b2 = a2 &
b3 = a3 holds
for
f1 being
Morphism of
a1,
a2 for
g1 being
Morphism of
b1,
b2 st
g1 = f1 holds
for
f2 being
Morphism of
a2,
a3 for
g2 being
Morphism of
b2,
b3 st
g2 = f2 holds
f2 * f1 = g2 * g1 )