:: deftheorem defines antimultiplicative CAT_6:def 24 :
for C, D being with_identities CategoryStr
for F being Functor of C,D holds
( F is antimultiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds
( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) ) );