theorem Th37: :: FUNCTOR0:37

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is id-preserving