theorem Th47: :: CAT_7:47

for C, C1, C2, D being category
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