let A, B be non empty AltCatStr ; for F being FunctorStr of A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
let F be FunctorStr of A,B; ( F is bijective implies ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) )
assume A1:
F is bijective
; ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
then A2:
F is injective
by FUNCTOR0:def 35;
then
F is one-to-one
by FUNCTOR0:def 33;
then A3:
the ObjectMap of F is one-to-one
by FUNCTOR0:def 6;
F is surjective
by A1, FUNCTOR0:def 35;
then
F is onto
by FUNCTOR0:def 34;
then A4:
the ObjectMap of F is onto
by FUNCTOR0:def 7;
F is faithful
by A2, FUNCTOR0:def 33;
hence
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )
by A3, A4, FUNCTOR0:def 30; verum