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
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
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 A2: FunctorStr(# the ObjectMap of G,the MorphMap of G #) = F " ; :: thesis: F * G = id B
set I1 = [:the carrier of A,the carrier of A:];
set I2 = [:the carrier of B,the carrier of B:];
the ObjectMap of (F * G) = the ObjectMap of F * the ObjectMap of G by FUNCTOR0:def 37;
then A3: the ObjectMap of (F * G) = the ObjectMap of F * (the ObjectMap of F " ) by A1, A2, 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;
F is surjective by A1, FUNCTOR0:def 36;
then F is onto by FUNCTOR0:def 35;
then A5: the ObjectMap of F is onto by FUNCTOR0:def 8;
set OM = the ObjectMap of F;
A6: dom the ObjectMap of F = [:the carrier of A,the carrier of A:] by FUNCT_2:def 1;
A7: rng the ObjectMap of F = [:the carrier of B,the carrier of B:] by A5, FUNCT_2:def 3;
reconsider OM = the ObjectMap of F as bifunction of the carrier of A,the carrier of B ;
A8: the ObjectMap of (F * G) = id [:the carrier of B,the carrier of B:] by A3, A4, A7, FUNCT_1:61;
F is injective by A1, FUNCTOR0:def 36;
then A9: F is faithful by FUNCTOR0:def 34;
then A10: the MorphMap of F is "1-1" by FUNCTOR0:def 31;
F is surjective by A1, FUNCTOR0:def 36;
then A11: ( F is full & F is onto ) by FUNCTOR0:def 35;
FunctorStr(# the ObjectMap of G,the MorphMap of G #) is bijective by A1, A2, 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;
consider k being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F such that
A13: k = the MorphMap of F and
A14: the MorphMap of (F " ) = (k "" ) * (the ObjectMap of F " ) by A1, FUNCTOR0:def 39;
consider f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F such that
A15: f = the MorphMap of F and
A16: f is "onto" by A11, FUNCTOR0:def 33;
A17: the ObjectMap of G = the ObjectMap of F " by A1, A2, FUNCTOR0:def 39;
set OMG = the ObjectMap of G;
A18: the MorphMap of (F * G) = (f * the ObjectMap of G) ** ((k "" ) * the ObjectMap of G) by A2, A14, A15, A17, FUNCTOR0:def 37;
A19: [:the carrier of B,the carrier of B:] = dom ((f * the ObjectMap of G) ** ((k "" ) * the ObjectMap of G)) by PARTFUN1:def 4;
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 A20: 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
A21: dom the ObjectMap of G = [:the carrier of B,the carrier of B:] by FUNCT_2:def 1;
then A22: (f * the ObjectMap of G) . i = k . (the ObjectMap of G . i) by A13, A15, A20, FUNCT_1:23;
A23: the ObjectMap of G . i in [:the carrier of A,the carrier of A:]

proof

rng the ObjectMap of G = [:the carrier of A,the carrier of A:] by A12, FUNCT_2:def 3;
hence the ObjectMap of G . i in [:the carrier of A,the carrier of A:] by A20, A21, FUNCT_1:def 5; :: thesis: verum

end;

A24: ((k "" ) * the ObjectMap of G) . i = (k "" ) . (the ObjectMap of G . i) by A20, A21, FUNCT_1:23
.= (k . (the ObjectMap of G . i)) " by A10, A13, A15, A16, A23, MSUALG_3:def 5 ;
A25: f . (the ObjectMap of G . i) is one-to-one

proof

A26: f is "1-1" by A9, A15, FUNCTOR0:def 31;
dom f = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
hence f . (the ObjectMap of G . i) is one-to-one by A23, A26, MSUALG_3:def 2; :: thesis: verum

end;

A27: rng (f . (the ObjectMap of G . i)) = (the Arrows of B * the ObjectMap of F) . (the ObjectMap of G . i) by A16, A23, MSUALG_3:def 3
.= the Arrows of B . (the ObjectMap of F . (the ObjectMap of G . i)) by A6, A23, FUNCT_1:23 ;
A28: the ObjectMap of F . (the ObjectMap of G . i) = (OM * (OM " )) . i by A17, A20, A21, FUNCT_1:23
.= (id [:the carrier of B,the carrier of B:]) . i by A4, A7, FUNCT_1:61
.= i by A20, FUNCT_1:35 ;
((f * the ObjectMap of G) ** ((k "" ) * the ObjectMap of G)) . i = (f . (the ObjectMap of G . i)) * ((f . (the ObjectMap of G . i)) " ) by A13, A15, A19, A20, A22, A24, PBOOLE:def 24
.= id (the Arrows of B . i) by A25, A27, A28, FUNCT_1:61
.= (id the Arrows of B) . i by A20, 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;

then the MorphMap of (F * G) = id the Arrows of B by A18, PBOOLE:3;
hence F * G = id B by A8, FUNCTOR0:def 30; :: thesis: verum