let A, B be category; :: thesis: for F being Functor of A,B st F is bijective holds

for G being Functor of B,A st F * G = id B holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

let F be Functor of A,B; :: thesis: ( F is bijective implies for G being Functor of B,A st F * G = id B holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume A1: F is bijective ; :: thesis: for G being Functor of B,A st F * G = id B holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

then reconsider FF = F " as feasible FunctorStr over B,A by FUNCTOR0:35;

A2: (F ") * F = id A by A1, FUNCTOR1:19;

let G be Functor of B,A; :: thesis: ( F * G = id B implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume F * G = id B ; :: thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

then (id A) * G = FF * (id B) by A2, FUNCTOR0:32

.= F " by FUNCTOR3:5 ;

hence FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by FUNCTOR3:4; :: thesis: verum

for G being Functor of B,A st F * G = id B holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

let F be Functor of A,B; :: thesis: ( F is bijective implies for G being Functor of B,A st F * G = id B holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume A1: F is bijective ; :: thesis: for G being Functor of B,A st F * G = id B holds

FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

then reconsider FF = F " as feasible FunctorStr over B,A by FUNCTOR0:35;

A2: (F ") * F = id A by A1, FUNCTOR1:19;

let G be Functor of B,A; :: thesis: ( F * G = id B implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )

assume F * G = id B ; :: thesis: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "

then (id A) * G = FF * (id B) by A2, FUNCTOR0:32

.= F " by FUNCTOR3:5 ;

hence FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " by FUNCTOR3:4; :: thesis: verum