theorem
for
C being non
empty category for
c1,
c2,
a,
b being
Object of
C for
p1 being
Morphism of
a,
c1 for
p2 being
Morphism of
a,
c2 for
q1 being
Morphism of
b,
c1 for
q2 being
Morphism of
b,
c2 st
Hom (
a,
c1)
<> {} &
Hom (
a,
c2)
<> {} &
Hom (
b,
c1)
<> {} &
Hom (
b,
c2)
<> {} &
a,
p1,
p2 is_product_of c1,
c2 &
b,
q1,
q2 is_product_of c1,
c2 holds
a,
b are_isomorphic