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 A1, FUNCTOR0:def 38;
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 A1, A10, FUNCTOR0:def 38;
FunctorStr(# the ObjectMap of G, the MorphMap of G #) is bijective by A1, A10, FUNCTOR0:35;
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 A2, A8, A16, FUNCT_1:13;
rng the ObjectMap of G = [: the carrier of A, the carrier of A:] by A12, FUNCT_2:def 3;
then A19: the ObjectMap of G . i in [: the carrier of A, the carrier of A:] by A16, A17, FUNCT_1:def 3;
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 A13, A19, FUNCT_1:13 ;
A21: the ObjectMap of F . ( the ObjectMap of G . i) = (OM * (OM ")) . i by A11, A16, A17, FUNCT_1:13
.= (id [: the carrier of B, the carrier of B:]) . i by A4, A5, FUNCT_1:39
.= i by A16, FUNCT_1:18 ;
( f is "1-1" & dom f = [: the carrier of A, the carrier of A:] ) by A6, A8, PARTFUN1:def 2;
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 A16, A17, FUNCT_1:13
.= (k . ( the ObjectMap of G . i)) " by A7, A2, A8, A9, A19, MSUALG_3:def 4 ;
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 A2, A8, A14, A16, A18, PBOOLE:def 19
.= id ( the Arrows of B . i) by A22, A20, A21, FUNCT_1:39
.= (id the Arrows of B) . i by A16, MSUALG_3:def 1 ;
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 A10, A3, A8, A11, FUNCTOR0:def 36;
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 A1, A10, FUNCTOR0:def 38;
then the ObjectMap of (F * G) = id [: the carrier of B, the carrier of B:] by A4, A5, FUNCT_1:39;
hence F * G = id B by A23, FUNCTOR0:def 29; :: thesis: verum