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