let C, C1, C2, D, E 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
for Q1 being Functor of E,C1
for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds
D ~= E
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
for Q1 being Functor of E,C1
for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds
D ~= E
let F2 be Functor of C2,C; :: thesis: for P1 being Functor of D,C1
for P2 being Functor of D,C2
for Q1 being Functor of E,C1
for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds
D ~= E
let P1 be Functor of D,C1; :: thesis: for P2 being Functor of D,C2
for Q1 being Functor of E,C1
for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds
D ~= E
let P2 be Functor of D,C2; :: thesis: for Q1 being Functor of E,C1
for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds
D ~= E
let Q1 be Functor of E,C1; :: thesis: for Q2 being Functor of E,C2 st F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 holds
D ~= E
let Q2 be Functor of E,C2; :: thesis: ( F1 is covariant & F2 is covariant & P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & D,P1,P2 is_pullback_of F1,F2 & E,Q1,Q2 is_pullback_of F1,F2 implies D ~= E )
assume A1: ( F1 is covariant & F2 is covariant ) ; :: thesis: ( not P1 is covariant or not P2 is covariant or not Q1 is covariant or not Q2 is covariant or not D,P1,P2 is_pullback_of F1,F2 or not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )
assume A2: ( P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant ) ; :: thesis: ( not D,P1,P2 is_pullback_of F1,F2 or not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )
assume A3: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: ( not E,Q1,Q2 is_pullback_of F1,F2 or D ~= E )
assume A4: E,Q1,Q2 is_pullback_of F1,F2 ; :: thesis: D ~= E
ex FF being Functor of D,E ex GG being Functor of E,D st
( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )

proof

A5: ( F1 (*) P1 = F2 (*) P2 & ( for D0 being category
for G1 being Functor of D0,C1
for G2 being Functor of D0,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D0,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D0,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) ) ) by A2, A1, A3, Def20;
A6: ( F1 (*) Q1 = F2 (*) Q2 & ( for D0 being category
for G1 being Functor of D0,C1
for G2 being Functor of D0,C2 st G1 is covariant & G2 is covariant & F1 (*) G1 = F2 (*) G2 holds
ex H being Functor of D0,E st
( H is covariant & Q1 (*) H = G1 & Q2 (*) H = G2 & ( for H1 being Functor of D0,E st H1 is covariant & Q1 (*) H1 = G1 & Q2 (*) H1 = G2 holds
H = H1 ) ) ) ) by A2, A1, A4, Def20;
consider FF being Functor of D,E such that
A7: ( FF is covariant & Q1 (*) FF = P1 & Q2 (*) FF = P2 & ( for H1 being Functor of D,E st H1 is covariant & Q1 (*) H1 = P1 & Q2 (*) H1 = P2 holds
FF = H1 ) ) by A2, A5, A1, A4, Def20;
consider GG being Functor of E,D such that
A8: ( GG is covariant & P1 (*) GG = Q1 & P2 (*) GG = Q2 & ( for H1 being Functor of E,D st H1 is covariant & P1 (*) H1 = Q1 & P2 (*) H1 = Q2 holds
GG = H1 ) ) by A2, A6, A1, A3, Def20;
take FF ; :: thesis: ex GG being Functor of E,D st
( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )
take GG ; :: thesis: ( FF is covariant & GG is covariant & GG (*) FF = id D & FF (*) GG = id E )
thus ( FF is covariant & GG is covariant ) by A7, A8; :: thesis: ( GG (*) FF = id D & FF (*) GG = id E )
set G11 = Q1 (*) FF;
set G12 = Q2 (*) FF;
consider H1 being Functor of D,D such that
A9: ( H1 is covariant & P1 (*) H1 = Q1 (*) FF & P2 (*) H1 = Q2 (*) FF & ( for H being Functor of D,D st H is covariant & P1 (*) H = Q1 (*) FF & P2 (*) H = Q2 (*) FF holds
H1 = H ) ) by A2, A5, A7;
A10: P1 (*) (GG (*) FF) = Q1 (*) FF by A2, A7, A8, Th10;
A11: P2 (*) (GG (*) FF) = Q2 (*) FF by A2, A7, A8, Th10;
A12: P1 (*) (id D) = Q1 (*) FF by A2, A7, Th11;
A13: P2 (*) (id D) = Q2 (*) FF by A2, A7, Th11;
thus GG (*) FF = H1 by A9, A10, A11, A7, A8, CAT_6:35
.= id D by A9, A12, A13 ; :: thesis: FF (*) GG = id E
set G21 = P1 (*) GG;
set G22 = P2 (*) GG;
consider H2 being Functor of E,E such that
A14: ( H2 is covariant & Q1 (*) H2 = P1 (*) GG & Q2 (*) H2 = P2 (*) GG & ( for H being Functor of E,E st H is covariant & Q1 (*) H = P1 (*) GG & Q2 (*) H = P2 (*) GG holds
H2 = H ) ) by A2, A6, A8;
A15: Q1 (*) (FF (*) GG) = P1 (*) GG by A2, A7, A8, Th10;
A16: Q2 (*) (FF (*) GG) = P2 (*) GG by A2, A7, A8, Th10;
A17: Q1 (*) (id E) = P1 (*) GG by A2, A8, Th11;
A18: Q2 (*) (id E) = P2 (*) GG by A2, A8, Th11;
thus FF (*) GG = H2 by A14, A15, A16, A7, A8, CAT_6:35
.= id E by A14, A17, A18 ; :: thesis: verum

end;

hence D ~= E by CAT_6:def 28; :: thesis: verum