let C be 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 monomorphism holds
p2 is monomorphism
let c, c1, c2, d be 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 monomorphism holds
p2 is monomorphism
let f1 be 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 monomorphism holds
p2 is monomorphism
let f2 be 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 monomorphism holds
p2 is monomorphism
let p1 be 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 monomorphism holds
p2 is monomorphism
let p2 be Morphism of d,c2; ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & f1 is monomorphism implies p2 is monomorphism )
assume A1:
( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} )
; ( not d,p1,p2 is_pullback_of f1,f2 or not f1 is monomorphism or p2 is monomorphism )
assume A2:
d,p1,p2 is_pullback_of f1,f2
; ( not f1 is monomorphism or p2 is monomorphism )
then A3:
( 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 ) ) ) ) )
by A1, Def17;
assume A4:
f1 is monomorphism
; p2 is monomorphism
thus
Hom (d,c2) <> {}
by A1; CAT_7:def 5 for c being Object of C st Hom (c,d) <> {} holds
for g1, g2 being Morphism of c,d st p2 * g1 = p2 * g2 holds
g1 = g2
let d1 be Object of C; ( Hom (d1,d) <> {} implies for g1, g2 being Morphism of d1,d st p2 * g1 = p2 * g2 holds
g1 = g2 )
assume A5:
Hom (d1,d) <> {}
; for g1, g2 being Morphism of d1,d st p2 * g1 = p2 * g2 holds
g1 = g2
let q1, q2 be Morphism of d1,d; ( p2 * q1 = p2 * q2 implies q1 = q2 )
assume A6:
p2 * q1 = p2 * q2
; q1 = q2
set p11 = p1 * q1;
set p12 = p2 * q1;
A7:
( Hom (d1,c1) <> {} & Hom (d1,c2) <> {} )
by A1, A5, Th22;
f1 * (p1 * q1) =
(f1 * p1) * q1
by A5, A1, Th23
.=
f2 * (p2 * q1)
by A5, A3, A1, Th23
;
then consider h being Morphism of d1,d such that
A8:
( p1 * h = p1 * q1 & p2 * h = p2 * q1 & ( for h1 being Morphism of d1,d st p1 * h1 = p1 * q1 & p2 * h1 = p2 * q1 holds
h = h1 ) )
by A1, A2, Def17, A7;
A9:
q1 = h
by A8;
f1 * (p1 * q2) =
(f1 * p1) * q2
by A5, A1, Th23
.=
f2 * (p2 * q2)
by A5, A3, A1, Th23
.=
(f2 * p2) * q1
by A6, A5, A1, Th23
.=
f1 * (p1 * q1)
by A5, A3, A1, Th23
;
hence
q1 = q2
by A9, A8, A6, A7, A4; verum