theorem
for
C being non
empty category for
c,
c1,
c2,
d being
Object of
C for
f1 being
Morphism of
c1,
c for
f2 being
Morphism of
c2,
c for
p1 being
Morphism of
d,
c1 for
p2 being
Morphism of
d,
c2 st
Hom (
c1,
c)
<> {} &
Hom (
c2,
c)
<> {} &
Hom (
d,
c1)
<> {} &
Hom (
d,
c2)
<> {} &
d,
p1,
p2 is_pullback_of f1,
f2 &
f1 is
isomorphism holds
p2 is
isomorphism