let A, B be non empty AltCatStr ; :: thesis: for F being FunctorStr over A,B st F is bijective holds

( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

let F be FunctorStr over A,B; :: thesis: ( F is bijective implies ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) )

assume A1: F is bijective ; :: thesis: ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

then A2: F is injective ;

then F is one-to-one ;

then A3: the ObjectMap of F is one-to-one ;

F is surjective by A1;

then F is onto ;

then A4: the ObjectMap of F is onto ;

F is faithful by A2;

hence ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) by A3, A4; :: thesis: verum

( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

let F be FunctorStr over A,B; :: thesis: ( F is bijective implies ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) )

assume A1: F is bijective ; :: thesis: ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )

then A2: F is injective ;

then F is one-to-one ;

then A3: the ObjectMap of F is one-to-one ;

F is surjective by A1;

then F is onto ;

then A4: the ObjectMap of F is onto ;

F is faithful by A2;

hence ( the ObjectMap of F is bijective & the MorphMap of F is "1-1" ) by A3, A4; :: thesis: verum