let A, B be category; :: thesis: for F being covariant Functor of A,B st F is bijective holds
for G being covariant 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 "
let F be covariant Functor of A,B; :: thesis: ( F is bijective implies for G being covariant 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 " )
assume A1: F is bijective ; :: thesis: for G being covariant 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 "
let G be covariant Functor of B,A; :: thesis: ( ( 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 ) implies FunctorStr(# the ObjectMap of G,the MorphMap of G #) = F " )
assume that
A2: for b being object of B holds F . (G . b) = b and
A3: for a, b being object of B st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . (G . f) = f ; :: thesis: FunctorStr(# the ObjectMap of G,the MorphMap of G #) = F "

A4: now

let b be object of B; :: thesis: (F * G) . b = (id B) . b
thus (F * G) . b = F . (G . b) by FUNCTOR0:34
.= b by A2
.= (id B) . b by FUNCTOR0:30 ; :: thesis: verum

end;

now

let a, b be object of B; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (F * G) . f = (id B) . f )
assume A5: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (F * G) . f = (id B) . f
let f be Morphism of a,b; :: thesis: (F * G) . f = (id B) . f
thus (F * G) . f = F . (G . f) by A5, FUNCTOR3:6
.= f by A3, A5
.= (id B) . f by A5, FUNCTOR0:32 ; :: thesis: verum

end;

then F * G = id B by A4, YELLOW18:1;
hence FunctorStr(# the ObjectMap of G,the MorphMap of G #) = F " by A1, Th4; :: thesis: verum