let C, C1, C2, D be category; :: thesis: for F1 being Functor of C1,C

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let F2 be Functor of C2,C; :: thesis: for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let P2 be Functor of D,C2; :: thesis: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism implies P2 is isomorphism )

assume A1: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant ) ; :: 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 category

for G1 being Functor of D1,C1

for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1 ) ) ) ) by A1, Def20;

assume A4: F1 is isomorphism ; :: thesis: P2 is isomorphism

consider G1 being Functor of C,C1 such that

A5: ( G1 is covariant & G1 (*) F1 = id C1 & F1 (*) G1 = id C ) by A4;

set G11 = G1 (*) F2;

set G22 = id C2;

A6: G1 (*) F2 is covariant by A5, A1, CAT_6:35;

A7: F1 (*) (G1 (*) F2) = (F1 (*) G1) (*) F2 by A5, A1, Th10

.= F2 by A5, A1, Th11

.= F2 (*) (id C2) by A1, Th11 ;

consider Q2 being Functor of C2,D such that

A8: ( Q2 is covariant & P1 (*) Q2 = G1 (*) F2 & P2 (*) Q2 = id C2 & ( for H1 being Functor of C2,D st H1 is covariant & P1 (*) H1 = G1 (*) F2 & P2 (*) H1 = id C2 holds

Q2 = H1 ) ) by A6, A2, A1, Def20, A7;

set G33 = (P1 (*) Q2) (*) P2;

A9: F2 (*) P2 is covariant by A1, CAT_6:35;

A10: (P1 (*) Q2) (*) P2 is covariant by A8, A6, A1, CAT_6:35;

F1 (*) ((P1 (*) Q2) (*) P2) = F1 (*) (G1 (*) (F2 (*) P2)) by A5, A8, A1, Th10

.= (F1 (*) G1) (*) (F2 (*) P2) by A9, A5, A4, Th10

.= F2 (*) P2 by A9, Th11, A5 ;

then consider H being Functor of D,D such that

( H is covariant & P1 (*) H = (P1 (*) Q2) (*) P2 & P2 (*) H = P2 ) and

A11: for H1 being Functor of D,D st H1 is covariant & P1 (*) H1 = (P1 (*) Q2) (*) P2 & P2 (*) H1 = P2 holds

H = H1 by A1, A2, A10, Def20;

A12: P1 (*) (id D) = P1 by A1, Th11

.= (G1 (*) F1) (*) P1 by A1, A5, Th11

.= G1 (*) (F1 (*) P1) by A1, A5, Th10

.= (P1 (*) Q2) (*) P2 by A8, A3, A1, A5, Th10 ;

A13: P2 (*) (id D) = P2 by A1, Th11;

A14: P1 (*) (Q2 (*) P2) = (P1 (*) Q2) (*) P2 by A1, A8, Th10;

P2 (*) (Q2 (*) P2) = (P2 (*) Q2) (*) P2 by A1, A8, Th10

.= P2 by A1, A8, Th11 ;

then H = Q2 (*) P2 by A11, A14, A1, A8, CAT_6:35;

hence P2 is isomorphism by A8, A13, A11, A12, A1; :: thesis: verum

for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let F1 be Functor of C1,C; :: thesis: for F2 being Functor of C2,C

for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let F2 be Functor of C2,C; :: thesis: for P1 being Functor of D,C1

for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism holds

P2 is isomorphism

let P2 be Functor of D,C2; :: thesis: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & D,P1,P2 is_pullback_of F1,F2 & F1 is isomorphism implies P2 is isomorphism )

assume A1: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant ) ; :: 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 category

for G1 being Functor of D1,C1

for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds

ex H being Functor of D1,D st

( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds

H = H1 ) ) ) ) by A1, Def20;

assume A4: F1 is isomorphism ; :: thesis: P2 is isomorphism

consider G1 being Functor of C,C1 such that

A5: ( G1 is covariant & G1 (*) F1 = id C1 & F1 (*) G1 = id C ) by A4;

set G11 = G1 (*) F2;

set G22 = id C2;

A6: G1 (*) F2 is covariant by A5, A1, CAT_6:35;

A7: F1 (*) (G1 (*) F2) = (F1 (*) G1) (*) F2 by A5, A1, Th10

.= F2 by A5, A1, Th11

.= F2 (*) (id C2) by A1, Th11 ;

consider Q2 being Functor of C2,D such that

A8: ( Q2 is covariant & P1 (*) Q2 = G1 (*) F2 & P2 (*) Q2 = id C2 & ( for H1 being Functor of C2,D st H1 is covariant & P1 (*) H1 = G1 (*) F2 & P2 (*) H1 = id C2 holds

Q2 = H1 ) ) by A6, A2, A1, Def20, A7;

set G33 = (P1 (*) Q2) (*) P2;

A9: F2 (*) P2 is covariant by A1, CAT_6:35;

A10: (P1 (*) Q2) (*) P2 is covariant by A8, A6, A1, CAT_6:35;

F1 (*) ((P1 (*) Q2) (*) P2) = F1 (*) (G1 (*) (F2 (*) P2)) by A5, A8, A1, Th10

.= (F1 (*) G1) (*) (F2 (*) P2) by A9, A5, A4, Th10

.= F2 (*) P2 by A9, Th11, A5 ;

then consider H being Functor of D,D such that

( H is covariant & P1 (*) H = (P1 (*) Q2) (*) P2 & P2 (*) H = P2 ) and

A11: for H1 being Functor of D,D st H1 is covariant & P1 (*) H1 = (P1 (*) Q2) (*) P2 & P2 (*) H1 = P2 holds

H = H1 by A1, A2, A10, Def20;

A12: P1 (*) (id D) = P1 by A1, Th11

.= (G1 (*) F1) (*) P1 by A1, A5, Th11

.= G1 (*) (F1 (*) P1) by A1, A5, Th10

.= (P1 (*) Q2) (*) P2 by A8, A3, A1, A5, Th10 ;

A13: P2 (*) (id D) = P2 by A1, Th11;

A14: P1 (*) (Q2 (*) P2) = (P1 (*) Q2) (*) P2 by A1, A8, Th10;

P2 (*) (Q2 (*) P2) = (P2 (*) Q2) (*) P2 by A1, A8, Th10

.= P2 by A1, A8, Th11 ;

then H = Q2 (*) P2 by A11, A14, A1, A8, CAT_6:35;

hence P2 is isomorphism by A8, A13, A11, A12, A1; :: thesis: verum