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