theorem :: CAT_8:38
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
F1 (*) (OrdC0-> C1) = F2 (*) (OrdC0-> C2) ;