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 G * F = id A 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 G * F = id A 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 G * F = id A 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 * FF = id B by A1, FUNCTOR1:18;

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

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

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

.= FunctorStr(# the ObjectMap of G, the MorphMap of G #) 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 G * F = id A 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 G * F = id A 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 G * F = id A 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 * FF = id B by A1, FUNCTOR1:18;

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

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

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

.= FunctorStr(# the ObjectMap of G, the MorphMap of G #) by FUNCTOR3:5 ;

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