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

P2 is monomorphism

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

P2 is monomorphism

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

P2 is monomorphism

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

P2 is monomorphism

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 monomorphism implies P2 is monomorphism )

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 monomorphism or P2 is monomorphism )

assume A2: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: ( not F1 is monomorphism or P2 is monomorphism )

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 monomorphism ; :: thesis: P2 is monomorphism

for D1 being category

for Q1, Q2 being Functor of D1,D st Q1 is covariant & Q2 is covariant & P2 (*) Q1 = P2 (*) Q2 holds

Q1 = Q2

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

P2 is monomorphism

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

P2 is monomorphism

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

P2 is monomorphism

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

P2 is monomorphism

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 monomorphism implies P2 is monomorphism )

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 monomorphism or P2 is monomorphism )

assume A2: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: ( not F1 is monomorphism or P2 is monomorphism )

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 monomorphism ; :: thesis: P2 is monomorphism

for D1 being category

for Q1, Q2 being Functor of D1,D st Q1 is covariant & Q2 is covariant & P2 (*) Q1 = P2 (*) Q2 holds

Q1 = Q2

proof

hence
P2 is monomorphism
by A1; :: thesis: verum
let D1 be category; :: thesis: for Q1, Q2 being Functor of D1,D st Q1 is covariant & Q2 is covariant & P2 (*) Q1 = P2 (*) Q2 holds

Q1 = Q2

let Q1, Q2 be Functor of D1,D; :: thesis: ( Q1 is covariant & Q2 is covariant & P2 (*) Q1 = P2 (*) Q2 implies Q1 = Q2 )

assume A5: ( Q1 is covariant & Q2 is covariant ) ; :: thesis: ( not P2 (*) Q1 = P2 (*) Q2 or Q1 = Q2 )

assume A6: P2 (*) Q1 = P2 (*) Q2 ; :: thesis: Q1 = Q2

set P11 = P1 (*) Q1;

set P12 = P2 (*) Q1;

A7: ( P1 (*) Q1 is covariant & P2 (*) Q1 is covariant ) by A1, A5, CAT_6:35;

F1 (*) (P1 (*) Q1) = (F1 (*) P1) (*) Q1 by A5, A1, Th10

.= F2 (*) (P2 (*) Q1) by A5, A3, A1, Th10 ;

then consider H being Functor of D1,D such that

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

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

A9: Q1 = H by A5, A8;

A10: P1 (*) Q2 is covariant by A5, A1, CAT_6:35;

F1 (*) (P1 (*) Q2) = (F1 (*) P1) (*) Q2 by A5, A1, Th10

.= F2 (*) (P2 (*) Q2) by A5, A3, A1, Th10

.= (F2 (*) P2) (*) Q1 by A6, A5, A1, Th10

.= F1 (*) (P1 (*) Q1) by A5, A3, A1, Th10 ;

hence Q1 = Q2 by A5, A9, A8, A6, A7, A10, A4; :: thesis: verum

end;Q1 = Q2

let Q1, Q2 be Functor of D1,D; :: thesis: ( Q1 is covariant & Q2 is covariant & P2 (*) Q1 = P2 (*) Q2 implies Q1 = Q2 )

assume A5: ( Q1 is covariant & Q2 is covariant ) ; :: thesis: ( not P2 (*) Q1 = P2 (*) Q2 or Q1 = Q2 )

assume A6: P2 (*) Q1 = P2 (*) Q2 ; :: thesis: Q1 = Q2

set P11 = P1 (*) Q1;

set P12 = P2 (*) Q1;

A7: ( P1 (*) Q1 is covariant & P2 (*) Q1 is covariant ) by A1, A5, CAT_6:35;

F1 (*) (P1 (*) Q1) = (F1 (*) P1) (*) Q1 by A5, A1, Th10

.= F2 (*) (P2 (*) Q1) by A5, A3, A1, Th10 ;

then consider H being Functor of D1,D such that

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

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

A9: Q1 = H by A5, A8;

A10: P1 (*) Q2 is covariant by A5, A1, CAT_6:35;

F1 (*) (P1 (*) Q2) = (F1 (*) P1) (*) Q2 by A5, A1, Th10

.= F2 (*) (P2 (*) Q2) by A5, A3, A1, Th10

.= (F2 (*) P2) (*) Q1 by A6, A5, A1, Th10

.= F1 (*) (P1 (*) Q1) by A5, A3, A1, Th10 ;

hence Q1 = Q2 by A5, A9, A8, A6, A7, A10, A4; :: thesis: verum