let A, B be category; 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; ( 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
; 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; ( G * F = id A implies FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " )
assume
G * F = id A
; 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; verum