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 )

proof

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;

hence d,e are_isomorphic ; :: thesis: verum