let A, B be non empty transitive with_units reflexive AltCatStr ; :: thesis: for F being feasible FunctorStr over A,B st F is bijective holds
(F ") * F = id A
set I1 = [: the carrier of A, the carrier of A:];
let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies (F ") * F = id A )
assume A1: F is bijective ; :: thesis: (F ") * F = id A
consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A2: f = the MorphMap of F and
A3: the MorphMap of (F ") = (f "") * ( the ObjectMap of F ") by A1, FUNCTOR0:def 38;
set OM = the ObjectMap of F;
A4: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;
A5: the Arrows of A is_transformable_to the Arrows of B * the ObjectMap of F

proof

let i be set ; :: according to PZFMISC1:def 3 :: thesis: ( not i in [: the carrier of A, the carrier of A:] or not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )
assume A6: i in [: the carrier of A, the carrier of A:] ; :: thesis: ( not ( the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )
then consider o1, o2 being object such that
A7: ( o1 in the carrier of A & o2 in the carrier of A ) and
A8: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as Object of A by A7;
A9: the Arrows of A . i = the Arrows of A . (o1,o2) by A8
.= <^o1,o2^> by ALTCAT_1:def 1 ;
assume ( the Arrows of B * the ObjectMap of F) . i = {} ; :: thesis: the Arrows of A . i = {}
then the Arrows of B . ( the ObjectMap of F . (o1,o2)) = {} by A6, A8, FUNCT_2:15;
hence the Arrows of A . i = {} by A9, FUNCTOR0:def 11; :: thesis: verum

end;

F is injective by A1;
then F is faithful ;
then A10: the MorphMap of F is "1-1" ;
for i being object st i in [: the carrier of A, the carrier of A:] holds
((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i

proof

let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i )
assume A11: i in [: the carrier of A, the carrier of A:] ; :: thesis: ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i
then ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . ((id [: the carrier of A, the carrier of A:]) . i) by FUNCT_2:15
.= (f "") . i by A11, FUNCT_1:18 ;
hence ((f "") * (id [: the carrier of A, the carrier of A:])) . i = (f "") . i ; :: thesis: verum

end;

then A12: (f "") * (id [: the carrier of A, the carrier of A:]) = f "" ;
F is injective by A1;
then F is one-to-one ;
then A13: the ObjectMap of F is one-to-one ;
the ObjectMap of ((F ") * F) = the ObjectMap of (F ") * the ObjectMap of F by FUNCTOR0:def 36;
then the ObjectMap of ((F ") * F) = ( the ObjectMap of F ") * the ObjectMap of F by A1, FUNCTOR0:def 38;
then A14: the ObjectMap of ((F ") * F) = id [: the carrier of A, the carrier of A:] by A13, A4, FUNCT_1:39;
F is surjective by A1;
then ( F is full & F is onto ) ;
then A15: ex k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( k = the MorphMap of F & k is "onto" ) ;
the MorphMap of ((F ") * F) = (((f "") * ( the ObjectMap of F ")) * the ObjectMap of F) ** f by A2, A3, FUNCTOR0:def 36
.= ((f "") * (( the ObjectMap of F ") * the ObjectMap of F)) ** f by RELAT_1:36 ;
then the MorphMap of ((F ") * F) = ((f "") * (id [: the carrier of A, the carrier of A:])) ** f by A13, A4, FUNCT_1:39;
then the MorphMap of ((F ") * F) = id the Arrows of A by A5, A2, A10, A15, A12, Lm1;
hence (F ") * F = id A by A14, FUNCTOR0:def 29; :: thesis: verum