for A, B being category
for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for b being Object of B holds F . (G . b) = b ) & ( for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "