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 ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)

set CCA = [: the carrier of A, the carrier of A:];
set CCB = [: the carrier of B, the carrier of B:];
let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) )
assume A1: F is bijective ; :: thesis: (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
A2: F is injective by A1;
then F is one-to-one ;
then A3: the ObjectMap of F is one-to-one ;
A4: F " is bijective by ;
then F " is surjective ;
then A5: F " is full ;
F " is injective by A4;
then A6: F " is faithful ;
A7: the ObjectMap of (F ") " = ( the ObjectMap of F ") " by
.= the ObjectMap of F by ;
F is faithful by A2;
then A8: the MorphMap of F is "1-1" ;
A9: F is surjective by A1;
then F is onto ;
then the ObjectMap of F is onto ;
then A10: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def 3;
A11: F is full by A9;
the MorphMap of ((F ") ") = the MorphMap of F
proof
A12: ex kk being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") st
( kk = the MorphMap of (F ") & kk is "onto" ) by A5;
A13: 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" ) by A11;
consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") such that
A14: f = the MorphMap of (F ") and
A15: the MorphMap of ((F ") ") = (f "") * ( the ObjectMap of (F ") ") by ;
consider g being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A16: g = the MorphMap of F and
A17: the MorphMap of (F ") = (g "") * ( the ObjectMap of F ") by ;
A18: f is "1-1" by ;
for i being object st i in [: the carrier of A, the carrier of A:] holds
((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i
proof
A19: the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by ;
let i be object ; :: thesis: ( i in [: the carrier of A, the carrier of A:] implies ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i )
assume A20: i in [: the carrier of A, the carrier of A:] ; :: thesis: ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i
then A21: the ObjectMap of F . i in [: the carrier of B, the carrier of B:] by FUNCT_2:5;
the ObjectMap of F " is Function of [: the carrier of B, the carrier of B:],[: the carrier of A, the carrier of A:] by ;
then A22: ( the ObjectMap of F ") . ( the ObjectMap of F . i) in [: the carrier of A, the carrier of A:] by ;
A23: g . i is one-to-one by ;
((f "") * ( the ObjectMap of (F ") ")) . i = (f "") . ( the ObjectMap of F . i) by
.= ( the MorphMap of (F ") . ( the ObjectMap of F . i)) " by
.= ((g "") . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) " by
.= ((g . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) ") " by
.= ((g . i) ") " by
.= the MorphMap of F . i by ;
hence ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i ; :: thesis: verum
end;
hence the MorphMap of ((F ") ") = the MorphMap of F by A15; :: thesis: verum
end;
hence (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by ; :: thesis: verum