let A, B be non empty transitive with_units reflexive AltCatStr ; :: thesis: for F being feasible FunctorStr of A,B st F is bijective holds
for G being feasible FunctorStr of 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 of A,B; :: thesis: ( F is bijective implies for G being feasible FunctorStr of 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 of 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 39;
F is injective by A1, FUNCTOR0:def 36;
then F is one-to-one by FUNCTOR0:def 34;
then A4: the ObjectMap of F is one-to-one by FUNCTOR0:def 7;
set OM = the ObjectMap of F;
F is surjective by A1, FUNCTOR0:def 36;
then F is onto by FUNCTOR0:def 35;
then the ObjectMap of F is onto by FUNCTOR0:def 8;
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, FUNCTOR0:def 36;
then A6: F is faithful by FUNCTOR0:def 34;
then A7: the MorphMap of F is "1-1" by FUNCTOR0:def 31;
F is surjective by A1, FUNCTOR0:def 36;
then ( F is full & F is onto ) by FUNCTOR0:def 35;
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" by FUNCTOR0:def 33;
let G be feasible FunctorStr of 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 39;
FunctorStr(# the ObjectMap of G,the MorphMap of G #) is bijective by A1, A10, FUNCTOR0:36;
then FunctorStr(# the ObjectMap of G,the MorphMap of G #) is surjective by FUNCTOR0:def 36;
then ( FunctorStr(# the ObjectMap of G,the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G,the MorphMap of G #) is onto ) by FUNCTOR0:def 35;
then A12: the ObjectMap of G is onto by FUNCTOR0:def 8;
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 4;
A15: for i being set 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 set ; :: 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:23;
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 5;
then A20: rng (f . (the ObjectMap of G . i)) = (the Arrows of B * the ObjectMap of F) . (the ObjectMap of G . i) by A9, MSUALG_3:def 3
.= the Arrows of B . (the ObjectMap of F . (the ObjectMap of G . i)) by A13, A19, FUNCT_1:23 ;
A21: the ObjectMap of F . (the ObjectMap of G . i) = (OM * (OM " )) . i by A11, A16, A17, FUNCT_1:23
.= (id [:the carrier of B,the carrier of B:]) . i by A4, A5, FUNCT_1:61
.= i by A16, FUNCT_1:35 ;
( f is "1-1" & dom f = [:the carrier of A,the carrier of A:] ) by A6, A8, FUNCTOR0:def 31, PARTFUN1:def 4;
then A22: f . (the ObjectMap of G . i) is one-to-one by A19, MSUALG_3:def 2;
((k "" ) * the ObjectMap of G) . i = (k "" ) . (the ObjectMap of G . i) by A16, A17, FUNCT_1:23
.= (k . (the ObjectMap of G . i)) " by A7, A2, A8, A9, A19, MSUALG_3:def 5 ;
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 24
.= id (the Arrows of B . i) by A22, A20, A21, FUNCT_1:61
.= (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 37;
then A23: the MorphMap of (F * G) = id the Arrows of B by A15, PBOOLE:3;
the ObjectMap of (F * G) = the ObjectMap of F * the ObjectMap of G by FUNCTOR0:def 37;
then the ObjectMap of (F * G) = the ObjectMap of F * (the ObjectMap of F " ) by A1, A10, FUNCTOR0:def 39;
then the ObjectMap of (F * G) = id [:the carrier of B,the carrier of B:] by A4, A5, FUNCT_1:61;
hence F * G = id B by A23, FUNCTOR0:def 30; :: thesis: verum