theorem Th52:
for
C,
C1,
C2 being
category for
F1 being
Functor of
C1,
C for
F2 being
Functor of
C2,
C st
F1 is
covariant &
F2 is
covariant holds
(
pr1 (
F1,
F2) is
covariant &
pr2 (
F1,
F2) is
covariant &
[|F1,F2|],
pr1 (
F1,
F2),
pr2 (
F1,
F2)
is_pullback_of F1,
F2 )