theorem Th23: :: FUNCTOR0:23

for C1, C2 being non empty AltGraph
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1 holds the ObjectMap of F . (o1,o2) = [(F . o2),(F . o1)]