let C be category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) <> {} ) ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: p2 is monomorphism

thus Hom (d,c2) <> {} by A1; :: according to CAT_7:def 5 :: thesis: 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; :: thesis: ( 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) <> {} ; :: thesis: for g1, g2 being Morphism of d1,d st p2 * g1 = p2 * g2 holds

g1 = g2

let q1, q2 be Morphism of d1,d; :: thesis: ( p2 * q1 = p2 * q2 implies q1 = q2 )

assume A6: p2 * q1 = p2 * q2 ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) <> {} ) ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: p2 is monomorphism

thus Hom (d,c2) <> {} by A1; :: according to CAT_7:def 5 :: thesis: 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; :: thesis: ( 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) <> {} ; :: thesis: for g1, g2 being Morphism of d1,d st p2 * g1 = p2 * g2 holds

g1 = g2

let q1, q2 be Morphism of d1,d; :: thesis: ( p2 * q1 = p2 * q2 implies q1 = q2 )

assume A6: p2 * q1 = p2 * q2 ; :: thesis: 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; :: thesis: verum