theorem Th40: :: FUNCTOR0:40

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds
for o1, o2 being Object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m