theorem Th5: :: YELLOW20:5

for A, B being category
for F being Functor of A,B st F is bijective holds
for G being Functor of B,A st G * F = id A holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "