let C1, C2 be category; :: thesis: for F being Functor of C1,C2 st F is isomorphism holds
F is bijective
let F be Functor of C1,C2; :: thesis: ( F is isomorphism implies F is bijective )
assume A1: F is isomorphism ; :: thesis: F is bijective
then A2: F is covariant by CAT_7:def 19;
consider G being Functor of C2,C1 such that
A3: ( G is covariant & G (*) F = id C1 & F (*) G = id C2 ) by A1, CAT_7:def 19;
A4: ( F * G = id C1 & G * F = id C2 ) by A2, A3, CAT_6:def 27;
( id C1 = id the carrier of C1 & id C2 = id the carrier of C2 ) by STRUCT_0:def 4;
then ( F is one-to-one & F is onto ) by A4, FUNCT_2:23;
hence F is bijective ; :: thesis: verum