let A, B be category; for F being contravariant Functor of A,B st F is bijective holds
for G being contravariant Functor of B,A st ( for a being Object of A holds G . (F . a) = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let F be contravariant Functor of A,B; ( F is bijective implies for G being contravariant Functor of B,A st ( for a being Object of A holds G . (F . a) = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume A1:
F is bijective
; for G being contravariant Functor of B,A st ( for a being Object of A holds G . (F . a) = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) holds
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
let G be contravariant Functor of B,A; ( ( for a being Object of A holds G . (F . a) = a ) & ( for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f ) implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume that
A2:
for b being Object of A holds G . (F . b) = b
and
A3:
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . (F . f) = f
; FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
hence
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
by A1, A4, Th5, YELLOW18:1; verum