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
for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B

set I1 = [: the carrier of A, the carrier of A:];
set I2 = [: the carrier of B, the carrier of B:];
let F be feasible FunctorStr over A,B; :: thesis: ( F is bijective implies for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B )

assume A1: F is bijective ; :: thesis: for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B

consider k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A2: k = the MorphMap of F and
A3: the MorphMap of (F ") = (k "") * ( the ObjectMap of F ") by ;
F is injective by A1;
then F is one-to-one ;
then A4: the ObjectMap of F is one-to-one ;
set OM = the ObjectMap of F;
F is surjective by A1;
then F is onto ;
then the ObjectMap of F is onto ;
then A5: rng the ObjectMap of F = [: the carrier of B, the carrier of B:] by FUNCT_2:def 3;
F is injective by A1;
then A6: F is faithful ;
then A7: the MorphMap of F is "1-1" ;
F is surjective by A1;
then ( F is full & F is onto ) ;
then consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A8: f = the MorphMap of F and
A9: f is "onto" ;
let G be feasible FunctorStr over B,A; :: thesis: ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " implies F * G = id B )
assume A10: FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " ; :: thesis: F * G = id B
A11: the ObjectMap of G = the ObjectMap of F " by ;
FunctorStr(# the ObjectMap of G, the MorphMap of G #) is bijective by ;
then FunctorStr(# the ObjectMap of G, the MorphMap of G #) is surjective ;
then ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G, the MorphMap of G #) is onto ) ;
then A12: the ObjectMap of G is onto ;
set OMG = the ObjectMap of G;
A13: dom the ObjectMap of F = [: the carrier of A, the carrier of A:] by FUNCT_2:def 1;
reconsider OM = the ObjectMap of F as bifunction of the carrier of A, the carrier of B ;
A14: [: the carrier of B, the carrier of B:] = dom ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) by PARTFUN1:def 2;
A15: for i being object st i in [: the carrier of B, the carrier of B:] holds
((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i
proof
let i be object ; :: thesis: ( i in [: the carrier of B, the carrier of B:] implies ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i )
assume A16: i in [: the carrier of B, the carrier of B:] ; :: thesis: ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i
A17: dom the ObjectMap of G = [: the carrier of B, the carrier of B:] by FUNCT_2:def 1;
then A18: (f * the ObjectMap of G) . i = k . ( the ObjectMap of G . i) by ;
rng the ObjectMap of G = [: the carrier of A, the carrier of A:] by ;
then A19: the ObjectMap of G . i in [: the carrier of A, the carrier of A:] by ;
then A20: rng (f . ( the ObjectMap of G . i)) = ( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of G . i) by A9
.= the Arrows of B . ( the ObjectMap of F . ( the ObjectMap of G . i)) by ;
A21: the ObjectMap of F . ( the ObjectMap of G . i) = (OM * (OM ")) . i by
.= (id [: the carrier of B, the carrier of B:]) . i by
.= i by ;
( f is "1-1" & dom f = [: the carrier of A, the carrier of A:] ) by ;
then A22: f . ( the ObjectMap of G . i) is one-to-one by A19;
((k "") * the ObjectMap of G) . i = (k "") . ( the ObjectMap of G . i) by
.= (k . ( the ObjectMap of G . i)) " by ;
then ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (f . ( the ObjectMap of G . i)) * ((f . ( the ObjectMap of G . i)) ") by
.= id ( the Arrows of B . i) by
.= (id the Arrows of B) . i by ;
hence ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i ; :: thesis: verum
end;
the MorphMap of (F * G) = (f * the ObjectMap of G) ** ((k "") * the ObjectMap of G) by ;
then A23: the MorphMap of (F * G) = id the Arrows of B by A15;
the ObjectMap of (F * G) = the ObjectMap of F * the ObjectMap of G by FUNCTOR0:def 36;
then the ObjectMap of (F * G) = the ObjectMap of F * ( the ObjectMap of F ") by ;
then the ObjectMap of (F * G) = id [: the carrier of B, the carrier of B:] by ;
hence F * G = id B by ; :: thesis: verum