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

proof

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;

hence P2 is monomorphism by A1; :: thesis: verum