theorem Th13: :: CAT_8:13

for C1, C2 being with_identities CategoryStr
for f1, f2 being morphism of C1
for F being Functor of C1,C2 st F is covariant & f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )