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 holds
D,P2,P1 is_pullback_of F2,F1
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 holds
D,P2,P1 is_pullback_of F2,F1
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 holds
D,P2,P1 is_pullback_of F2,F1
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 holds
D,P2,P1 is_pullback_of F2,F1
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 implies D,P2,P1 is_pullback_of F2,F1 )
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 D,P2,P1 is_pullback_of F2,F1 )
assume A2: D,P1,P2 is_pullback_of F1,F2 ; :: thesis: D,P2,P1 is_pullback_of F2,F1
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;
for D1 being category
for G1 being Functor of D1,C2
for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )

proof

let D1 be category; :: thesis: for G1 being Functor of D1,C2
for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
let G1 be Functor of D1,C2; :: thesis: for G2 being Functor of D1,C1 st G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 holds
ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
let G2 be Functor of D1,C1; :: thesis: ( G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 implies ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) ) )
assume A4: ( G1 is covariant & G2 is covariant & F2 (*) G1 = F1 (*) G2 ) ; :: thesis: ex H being Functor of D1,D st
( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
consider H being Functor of D1,D such that
A5: ( H is covariant & P1 (*) H = G2 & P2 (*) H = G1 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G2 & P2 (*) H1 = G1 holds
H = H1 ) ) by A4, A2, A1, Def20;
take H ; :: thesis: ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1 ) )
thus ( H is covariant & P2 (*) H = G1 & P1 (*) H = G2 ) by A5; :: thesis: for H1 being Functor of D1,D st H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 holds
H = H1
let H1 be Functor of D1,D; :: thesis: ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 implies H = H1 )
assume ( H1 is covariant & P2 (*) H1 = G1 & P1 (*) H1 = G2 ) ; :: thesis: H = H1
hence H = H1 by A5; :: thesis: verum

end;

hence D,P2,P1 is_pullback_of F2,F1 by A3, A1, Def20; :: thesis: verum