let C be non empty 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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism implies p2 is isomorphism )

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 isomorphism or p2 is isomorphism )

assume A2: d,p1,p2 is_pullback_of f1,f2 ; :: thesis: ( not f1 is isomorphism or p2 is isomorphism )

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 isomorphism ; :: thesis: p2 is isomorphism

consider g1 being Morphism of c,c1 such that

A5: ( g1 * f1 = id- c1 & f1 * g1 = id- c ) by A4;

set g11 = g1 * f2;

set g22 = id- c2;

A6: ( Hom (c2,c1) <> {} & Hom (c2,c2) <> {} & Hom (c1,c1) <> {} ) by A1, A4, Th22;

A7: f1 * (g1 * f2) = (f1 * g1) * f2 by A4, A1, Th23

.= f2 by A5, A1, Th18

.= f2 * (id- c2) by A1, Th18 ;

then A8: ( Hom (c2,d) <> {} & ex h being Morphism of c2,d st

( p1 * h = g1 * f2 & p2 * h = id- c2 & ( for h1 being Morphism of c2,d st p1 * h1 = g1 * f2 & p2 * h1 = id- c2 holds

h = h1 ) ) ) by A2, A1, Def17, A6;

consider q2 being Morphism of c2,d such that

A9: ( p1 * q2 = g1 * f2 & p2 * q2 = id- c2 & ( for h1 being Morphism of c2,d st p1 * h1 = g1 * f2 & p2 * h1 = id- c2 holds

q2 = h1 ) ) by A6, A2, A1, Def17, A7;

set g33 = (p1 * q2) * p2;

A10: Hom (d,c) <> {} by A1, Th22;

f1 * ((p1 * q2) * p2) = f1 * (g1 * (f2 * p2)) by A9, A4, A1, Th23

.= (f1 * g1) * (f2 * p2) by A10, A4, Th23

.= f2 * p2 by A10, Th18, A5 ;

then consider h being Morphism of d,d such that

( p1 * h = (p1 * q2) * p2 & p2 * h = p2 ) and

A11: for h1 being Morphism of d,d st p1 * h1 = (p1 * q2) * p2 & p2 * h1 = p2 holds

h = h1 by A1, A2, Def17;

A12: p1 * (id- d) = p1 by A1, Th18

.= (g1 * f1) * p1 by A1, A5, Th18

.= g1 * (f1 * p1) by A1, A4, Th23

.= (p1 * q2) * p2 by A9, A3, A4, A1, Th23 ;

A13: p2 * (id- d) = p2 by A1, Th18;

A14: p1 * (q2 * p2) = (p1 * q2) * p2 by A1, A8, Th23;

p2 * (q2 * p2) = (p2 * q2) * p2 by A1, A8, Th23

.= p2 by A1, A9, Th18 ;

then h = q2 * p2 by A11, A14;

hence p2 is isomorphism by A7, A9, A13, A11, A12, A2, A1, Def17, A6; :: 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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism holds

p2 is isomorphism

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 isomorphism implies p2 is isomorphism )

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 isomorphism or p2 is isomorphism )

assume A2: d,p1,p2 is_pullback_of f1,f2 ; :: thesis: ( not f1 is isomorphism or p2 is isomorphism )

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 isomorphism ; :: thesis: p2 is isomorphism

consider g1 being Morphism of c,c1 such that

A5: ( g1 * f1 = id- c1 & f1 * g1 = id- c ) by A4;

set g11 = g1 * f2;

set g22 = id- c2;

A6: ( Hom (c2,c1) <> {} & Hom (c2,c2) <> {} & Hom (c1,c1) <> {} ) by A1, A4, Th22;

A7: f1 * (g1 * f2) = (f1 * g1) * f2 by A4, A1, Th23

.= f2 by A5, A1, Th18

.= f2 * (id- c2) by A1, Th18 ;

then A8: ( Hom (c2,d) <> {} & ex h being Morphism of c2,d st

( p1 * h = g1 * f2 & p2 * h = id- c2 & ( for h1 being Morphism of c2,d st p1 * h1 = g1 * f2 & p2 * h1 = id- c2 holds

h = h1 ) ) ) by A2, A1, Def17, A6;

consider q2 being Morphism of c2,d such that

A9: ( p1 * q2 = g1 * f2 & p2 * q2 = id- c2 & ( for h1 being Morphism of c2,d st p1 * h1 = g1 * f2 & p2 * h1 = id- c2 holds

q2 = h1 ) ) by A6, A2, A1, Def17, A7;

set g33 = (p1 * q2) * p2;

A10: Hom (d,c) <> {} by A1, Th22;

f1 * ((p1 * q2) * p2) = f1 * (g1 * (f2 * p2)) by A9, A4, A1, Th23

.= (f1 * g1) * (f2 * p2) by A10, A4, Th23

.= f2 * p2 by A10, Th18, A5 ;

then consider h being Morphism of d,d such that

( p1 * h = (p1 * q2) * p2 & p2 * h = p2 ) and

A11: for h1 being Morphism of d,d st p1 * h1 = (p1 * q2) * p2 & p2 * h1 = p2 holds

h = h1 by A1, A2, Def17;

A12: p1 * (id- d) = p1 by A1, Th18

.= (g1 * f1) * p1 by A1, A5, Th18

.= g1 * (f1 * p1) by A1, A4, Th23

.= (p1 * q2) * p2 by A9, A3, A4, A1, Th23 ;

A13: p2 * (id- d) = p2 by A1, Th18;

A14: p1 * (q2 * p2) = (p1 * q2) * p2 by A1, A8, Th23;

p2 * (q2 * p2) = (p2 * q2) * p2 by A1, A8, Th23

.= p2 by A1, A9, Th18 ;

then h = q2 * p2 by A11, A14;

hence p2 is isomorphism by A7, A9, A13, A11, A12, A2, A1, Def17, A6; :: thesis: verum