let A, B be category; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
A4: now :: thesis: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (G * F) . f = (id A) . f
let a, b be Object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (G * F) . f = (id A) . f )
assume A5: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (G * F) . f = (id A) . f
let f be Morphism of a,b; :: thesis: (G * F) . f = (id A) . f
thus (G * F) . f = G . (F . f) by
.= f by A3, A5
.= (id A) . f by ; :: thesis: verum
end;
now :: thesis: for b being Object of A holds (G * F) . b = (id A) . b
let b be Object of A; :: thesis: (G * F) . b = (id A) . b
thus (G * F) . b = G . (F . b) by FUNCTOR0:33
.= b by A2
.= (id A) . b by FUNCTOR0:29 ; :: thesis: verum
end;
hence FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by ; :: thesis: verum