:: deftheorem Def17 defines is_pullback_of CAT_7:def 17 :
for C being category
for c, c1, c2, d being Object of C
for f1 being Morphism of c1,c st Hom (c1,c) <> {} holds
for f2 being Morphism of c2,c st Hom (c2,c) <> {} holds
for p1 being Morphism of d,c1 st Hom (d,c1) <> {} holds
for p2 being Morphism of d,c2 st Hom (d,c2) <> {} holds
( d,p1,p2 is_pullback_of f1,f2 iff ( f1 * p1 = f2 * p2 & ( for d1 being Object of C
for g1 being Morphism of d1,c1
for g2 being Morphism of d1,c2 st Hom (d1,c1) <> {} & Hom (d1,c2) <> {} & f1 * g1 = f2 * g2 holds
( Hom (d1,d) <> {} & ex h being Morphism of d1,d st
( p1 * h = g1 & p2 * h = g2 & ( for h1 being Morphism of d1,d st p1 * h1 = g1 & p2 * h1 = g2 holds
h = h1 ) ) ) ) ) );