let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being reflexive feasible id-preserving FunctorStr of A,B st F is bijective & F is coreflexive holds
F " is id-preserving
let F be reflexive feasible id-preserving FunctorStr of A,B; :: thesis: ( F is bijective & F is coreflexive implies F " is id-preserving )
assume A1: ( F is bijective & F is coreflexive ) ; :: thesis: F " is id-preserving
set G = F " ;
reconsider H = F " as reflexive feasible FunctorStr of B,A by A1, Th36, Th37;
A2: the ObjectMap of (F " ) = the ObjectMap of F " by A1, Def39;
consider f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F such that
A3: f = the MorphMap of F and
A4: the MorphMap of (F " ) = (f "" ) * (the ObjectMap of F " ) by A1, Def39;
let o be object of B; :: according to FUNCTOR0:def 21 :: thesis: (Morph-Map (F " ),o,o) . (idm o) = idm ((F " ) . o)
A5: F is injective by A1, Def36;
then F is one-to-one by Def34;
then A6: the ObjectMap of F is one-to-one by Def7;
F is faithful by A5, Def34;
then A7: the MorphMap of F is "1-1" by Def31;
F is surjective by A1, Def36;
then F is full by Def35;
then A8: ex f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) by Def33;
A9: [((F " ) . o),((F " ) . o)] in [:the carrier of A,the carrier of A:] by ZFMISC_1:106;
A10: [o,o] in [:the carrier of B,the carrier of B:] by ZFMISC_1:106;
then A11: [o,o] in dom the ObjectMap of (F " ) by FUNCT_2:def 1;
A12: the ObjectMap of (F * H) . o,o = (the ObjectMap of F * the ObjectMap of H) . [o,o] by Def37
.= (the ObjectMap of F * (the ObjectMap of F " )) . [o,o] by A1, Def39
.= (id (rng the ObjectMap of F)) . [o,o] by A6, FUNCT_1:61
.= (id (dom the ObjectMap of (F " ))) . [o,o] by A2, A6, FUNCT_1:55
.= (id [:the carrier of B,the carrier of B:]) . [o,o] by FUNCT_2:def 1
.= [o,o] by A10, FUNCT_1:35 ;
A13: F . ((F " ) . o) = (F * H) . o by Th34
.= o by A12, MCART_1:7 ;
dom the MorphMap of F = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then [((F " ) . o),((F " ) . o)] in dom the MorphMap of F by ZFMISC_1:106;
then A14: Morph-Map F,((F " ) . o),((F " ) . o) is one-to-one by A7, MSUALG_3:def 2;
[((F " ) . o),((F " ) . o)] in dom the ObjectMap of F by A9, FUNCT_2:def 1;
then (the Arrows of B * the ObjectMap of F) . [((F " ) . o),((F " ) . o)] = the Arrows of B . (the ObjectMap of F . ((F " ) . o),((F " ) . o)) by FUNCT_1:23
.= the Arrows of B . (F . ((F " ) . o)),(F . ((F " ) . o)) by Def11 ;
then A15: (the Arrows of B * the ObjectMap of F) . [((F " ) . o),((F " ) . o)] <> {} by ALTCAT_2:def 6;
Morph-Map F,((F " ) . o),((F " ) . o) is Function of (the Arrows of A . [((F " ) . o),((F " ) . o)]),((the Arrows of B * the ObjectMap of F) . [((F " ) . o),((F " ) . o)]) by A3, A9, PBOOLE:def 18;
then A16: dom (Morph-Map F,((F " ) . o),((F " ) . o)) = the Arrows of A . ((F " ) . o),((F " ) . o) by A15, FUNCT_2:def 1
.= <^((F " ) . o),((F " ) . o)^> by ALTCAT_1:def 2 ;
(the Arrows of A * the ObjectMap of (F " )) . [o,o] = the Arrows of A . (the ObjectMap of H . o,o) by A11, FUNCT_1:23
.= the Arrows of A . ((F " ) . o),((F " ) . o) by Def11 ;
then A17: (the Arrows of A * the ObjectMap of (F " )) . [o,o] <> {} by ALTCAT_2:def 6;
the MorphMap of (F " ) is ManySortedFunction of the Arrows of B,the Arrows of A * the ObjectMap of (F " ) by Def5;
then Morph-Map (F " ),o,o is Function of (the Arrows of B . [o,o]),((the Arrows of A * the ObjectMap of (F " )) . [o,o]) by A10, PBOOLE:def 18;
then A18: dom (Morph-Map (F " ),o,o) = the Arrows of B . o,o by A17, FUNCT_2:def 1
.= <^o,o^> by ALTCAT_1:def 2 ;
then A19: idm o in dom (Morph-Map (F " ),o,o) by ALTCAT_1:23;
A20: Morph-Map (F " ),o,o = (f "" ) . (the ObjectMap of (F " ) . o,o) by A2, A4, A11, FUNCT_1:23
.= (f "" ) . [(H . o),(H . o)] by Def11
.= (Morph-Map F,((F " ) . o),((F " ) . o)) " by A3, A7, A8, A9, MSUALG_3:def 5 ;
(Morph-Map (F " ),o,o) . (idm o) in rng (Morph-Map (F " ),o,o) by A19, FUNCT_1:def 5;
then A21: (Morph-Map (F " ),o,o) . (idm o) in dom (Morph-Map F,((F " ) . o),((F " ) . o)) by A14, A20, FUNCT_1:55;
(Morph-Map F,((F " ) . o),((F " ) . o)) . ((Morph-Map (F " ),o,o) . (idm o)) = ((Morph-Map F,((F " ) . o),((F " ) . o)) * (Morph-Map (F " ),o,o)) . (idm o) by A18, ALTCAT_1:23, FUNCT_1:23
.= (id (rng (Morph-Map F,((F " ) . o),((F " ) . o)))) . (idm o) by A14, A20, FUNCT_1:61
.= (id (dom (Morph-Map (F " ),o,o))) . (idm o) by A14, A20, FUNCT_1:55
.= idm (F . ((F " ) . o)) by A13, A18, ALTCAT_1:23, FUNCT_1:35
.= (Morph-Map F,((F " ) . o),((F " ) . o)) . (idm ((F " ) . o)) by Def21 ;
hence (Morph-Map (F " ),o,o) . (idm o) = idm ((F " ) . o) by A14, A16, A21, FUNCT_1:def 8; :: thesis: verum