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