let C be non empty category; :: thesis: for c, c1, c2, d, e 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

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let c, c1, c2, d, e 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

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

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

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let f2 be Morphism of c2,c; :: thesis: for p1 being Morphism of d,c1

for p2 being Morphism of d,c2

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let p1 be Morphism of d,c1; :: thesis: for p2 being Morphism of d,c2

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let p2 be Morphism of d,c2; :: thesis: for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let q1 be Morphism of e,c1; :: thesis: for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let q2 be Morphism of e,c2; :: thesis: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 implies d,e are_isomorphic )

assume A1: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} ) ; :: thesis: ( not d,p1,p2 is_pullback_of f1,f2 or not e,q1,q2 is_pullback_of f1,f2 or d,e are_isomorphic )

assume A2: d,p1,p2 is_pullback_of f1,f2 ; :: thesis: ( not e,q1,q2 is_pullback_of f1,f2 or d,e are_isomorphic )

assume A3: e,q1,q2 is_pullback_of f1,f2 ; :: thesis: d,e are_isomorphic

A4: ( 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, A2, Def17;

A5: ( f1 * q1 = f2 * q2 & ( for e1 being Object of C

for g1 being Morphism of e1,c1

for g2 being Morphism of e1,c2 st Hom (e1,c1) <> {} & Hom (e1,c2) <> {} & f1 * g1 = f2 * g2 holds

( Hom (e1,e) <> {} & ex h being Morphism of e1,e st

( q1 * h = g1 & q2 * h = g2 & ( for h1 being Morphism of e1,e st q1 * h1 = g1 & q2 * h1 = g2 holds

h = h1 ) ) ) ) ) by A1, A3, Def17;

ex ff being Morphism of d,e ex gg being Morphism of e,d st

( Hom (d,e) <> {} & Hom (e,d) <> {} & gg * ff = id- d & ff * gg = id- e )

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

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let c, c1, c2, d, e 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

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

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

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let f2 be Morphism of c2,c; :: thesis: for p1 being Morphism of d,c1

for p2 being Morphism of d,c2

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let p1 be Morphism of d,c1; :: thesis: for p2 being Morphism of d,c2

for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let p2 be Morphism of d,c2; :: thesis: for q1 being Morphism of e,c1

for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let q1 be Morphism of e,c1; :: thesis: for q2 being Morphism of e,c2 st Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 holds

d,e are_isomorphic

let q2 be Morphism of e,c2; :: thesis: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} & d,p1,p2 is_pullback_of f1,f2 & e,q1,q2 is_pullback_of f1,f2 implies d,e are_isomorphic )

assume A1: ( Hom (c1,c) <> {} & Hom (c2,c) <> {} & Hom (d,c1) <> {} & Hom (d,c2) <> {} & Hom (e,c1) <> {} & Hom (e,c2) <> {} ) ; :: thesis: ( not d,p1,p2 is_pullback_of f1,f2 or not e,q1,q2 is_pullback_of f1,f2 or d,e are_isomorphic )

assume A2: d,p1,p2 is_pullback_of f1,f2 ; :: thesis: ( not e,q1,q2 is_pullback_of f1,f2 or d,e are_isomorphic )

assume A3: e,q1,q2 is_pullback_of f1,f2 ; :: thesis: d,e are_isomorphic

A4: ( 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, A2, Def17;

A5: ( f1 * q1 = f2 * q2 & ( for e1 being Object of C

for g1 being Morphism of e1,c1

for g2 being Morphism of e1,c2 st Hom (e1,c1) <> {} & Hom (e1,c2) <> {} & f1 * g1 = f2 * g2 holds

( Hom (e1,e) <> {} & ex h being Morphism of e1,e st

( q1 * h = g1 & q2 * h = g2 & ( for h1 being Morphism of e1,e st q1 * h1 = g1 & q2 * h1 = g2 holds

h = h1 ) ) ) ) ) by A1, A3, Def17;

ex ff being Morphism of d,e ex gg being Morphism of e,d st

( Hom (d,e) <> {} & Hom (e,d) <> {} & gg * ff = id- d & ff * gg = id- e )

proof

hence
d,e are_isomorphic
; :: thesis: verum
consider f being Morphism of d,e such that

A6: ( q1 * f = p1 & q2 * f = p2 & ( for h1 being Morphism of d,e st q1 * h1 = p1 & q2 * h1 = p2 holds

f = h1 ) ) by A4, A1, A3, Def17;

consider g being Morphism of e,d such that

A7: ( p1 * g = q1 & p2 * g = q2 & ( for h1 being Morphism of e,d st p1 * h1 = q1 & p2 * h1 = q2 holds

g = h1 ) ) by A5, A1, A2, Def17;

take f ; :: thesis: ex gg being Morphism of e,d st

( Hom (d,e) <> {} & Hom (e,d) <> {} & gg * f = id- d & f * gg = id- e )

take g ; :: thesis: ( Hom (d,e) <> {} & Hom (e,d) <> {} & g * f = id- d & f * g = id- e )

thus A8: Hom (d,e) <> {} by A4, A1, A3, Def17; :: thesis: ( Hom (e,d) <> {} & g * f = id- d & f * g = id- e )

thus A9: Hom (e,d) <> {} by A5, A1, A2, Def17; :: thesis: ( g * f = id- d & f * g = id- e )

set g11 = q1 * f;

set g12 = q2 * f;

consider h1 being Morphism of d,d such that

A10: ( p1 * h1 = q1 * f & p2 * h1 = q2 * f & ( for h being Morphism of d,d st p1 * h = q1 * f & p2 * h = q2 * f holds

h1 = h ) ) by A1, A4, A6;

A11: p1 * (g * f) = q1 * f by A1, A7, A9, A8, Th23;

A12: p2 * (g * f) = q2 * f by A1, A7, A9, A8, Th23;

A13: p1 * (id- d) = q1 * f by A1, A6, Th18;

A14: p2 * (id- d) = q2 * f by A1, A6, Th18;

thus g * f = h1 by A10, A11, A12

.= id- d by A10, A13, A14 ; :: thesis: f * g = id- e

set g21 = p1 * g;

set g22 = p2 * g;

consider h2 being Morphism of e,e such that

A15: ( q1 * h2 = p1 * g & q2 * h2 = p2 * g & ( for h being Morphism of e,e st q1 * h = p1 * g & q2 * h = p2 * g holds

h2 = h ) ) by A1, A5, A7;

A16: q1 * (f * g) = p1 * g by A1, A6, A9, A8, Th23;

A17: q2 * (f * g) = p2 * g by A1, A6, A9, A8, Th23;

A18: q1 * (id- e) = p1 * g by A1, A7, Th18;

A19: q2 * (id- e) = p2 * g by A1, A7, Th18;

thus f * g = h2 by A15, A16, A17

.= id- e by A15, A18, A19 ; :: thesis: verum

end;A6: ( q1 * f = p1 & q2 * f = p2 & ( for h1 being Morphism of d,e st q1 * h1 = p1 & q2 * h1 = p2 holds

f = h1 ) ) by A4, A1, A3, Def17;

consider g being Morphism of e,d such that

A7: ( p1 * g = q1 & p2 * g = q2 & ( for h1 being Morphism of e,d st p1 * h1 = q1 & p2 * h1 = q2 holds

g = h1 ) ) by A5, A1, A2, Def17;

take f ; :: thesis: ex gg being Morphism of e,d st

( Hom (d,e) <> {} & Hom (e,d) <> {} & gg * f = id- d & f * gg = id- e )

take g ; :: thesis: ( Hom (d,e) <> {} & Hom (e,d) <> {} & g * f = id- d & f * g = id- e )

thus A8: Hom (d,e) <> {} by A4, A1, A3, Def17; :: thesis: ( Hom (e,d) <> {} & g * f = id- d & f * g = id- e )

thus A9: Hom (e,d) <> {} by A5, A1, A2, Def17; :: thesis: ( g * f = id- d & f * g = id- e )

set g11 = q1 * f;

set g12 = q2 * f;

consider h1 being Morphism of d,d such that

A10: ( p1 * h1 = q1 * f & p2 * h1 = q2 * f & ( for h being Morphism of d,d st p1 * h = q1 * f & p2 * h = q2 * f holds

h1 = h ) ) by A1, A4, A6;

A11: p1 * (g * f) = q1 * f by A1, A7, A9, A8, Th23;

A12: p2 * (g * f) = q2 * f by A1, A7, A9, A8, Th23;

A13: p1 * (id- d) = q1 * f by A1, A6, Th18;

A14: p2 * (id- d) = q2 * f by A1, A6, Th18;

thus g * f = h1 by A10, A11, A12

.= id- d by A10, A13, A14 ; :: thesis: f * g = id- e

set g21 = p1 * g;

set g22 = p2 * g;

consider h2 being Morphism of e,e such that

A15: ( q1 * h2 = p1 * g & q2 * h2 = p2 * g & ( for h being Morphism of e,e st q1 * h = p1 * g & q2 * h = p2 * g holds

h2 = h ) ) by A1, A5, A7;

A16: q1 * (f * g) = p1 * g by A1, A6, A9, A8, Th23;

A17: q2 * (f * g) = p2 * g by A1, A6, A9, A8, Th23;

A18: q1 * (id- e) = p1 * g by A1, A7, Th18;

A19: q2 * (id- e) = p2 * g by A1, A7, Th18;

thus f * g = h2 by A15, A16, A17

.= id- e by A15, A18, A19 ; :: thesis: verum