for C, C1, C2 being category
for F1 being Functor of C,C1
for F2 being Functor of C,C2 st F1 is covariant & F2 is covariant holds
(C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2