:: deftheorem Def16 defines . FUNCTOR0:def 16 :
for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1 st <^o1,o2^> <> {} & <^(F . o2),(F . o1)^> <> {} holds
for m being Morphism of o1,o2 holds F . m = (Morph-Map (F,o1,o2)) . m;