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 ) ) ) ) )