theorem
ex
C,
C1,
C2 being
Category ex
F1 being
Functor of
C1,
C ex
F2 being
Functor of
C2,
C st
for
D being
Category for
P1 being
Functor of
D,
C1 for
P2 being
Functor of
D,
C2 holds
( not
F1 * P1 = F2 * P2 or ex
D1 being
Category ex
G1 being
Functor of
D1,
C1 ex
G2 being
Functor of
D1,
C2 st
(
F1 * G1 = F2 * G2 & ( for
H being
Functor of
D1,
D holds
( not
P1 * H = G1 or not
P2 * H = G2 or ex
H1 being
Functor of
D1,
D st
(
P1 * H1 = G1 &
P2 * H1 = G2 & not
H = H1 ) ) ) ) )