theorem Th22: :: FUNCTOR0:22

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