let A, B be non empty transitive with_units AltCatStr ; for F being reflexive feasible id-preserving FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is id-preserving
let F be reflexive feasible id-preserving FunctorStr over A,B; ( F is bijective & F is coreflexive implies F " is id-preserving )
assume A1:
( F is bijective & F is coreflexive )
; F " is id-preserving
set G = F " ;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A2:
the ObjectMap of (F ") = the ObjectMap of F "
by A1, Def38;
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, Def38;
let o be Object of B; FUNCTOR0:def 20 (Morph-Map ((F "),o,o)) . (idm o) = idm ((F ") . o)
A5:
F is injective
by A1;
then
F is one-to-one
;
then A6:
the ObjectMap of F is one-to-one
;
F is faithful
by A5;
then A7:
the MorphMap of F is "1-1"
;
F is surjective
by A1;
then
F is full
;
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" )
;
A9:
[((F ") . o),((F ") . o)] in [: the carrier of A, the carrier of A:]
by ZFMISC_1:87;
A10:
[o,o] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
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 Def36
.=
( the ObjectMap of F * ( the ObjectMap of F ")) . [o,o]
by A1, Def38
.=
(id (rng the ObjectMap of F)) . [o,o]
by A6, FUNCT_1:39
.=
(id (dom the ObjectMap of (F "))) . [o,o]
by A2, A6, FUNCT_1:33
.=
(id [: the carrier of B, the carrier of B:]) . [o,o]
by FUNCT_2:def 1
.=
[o,o]
by A10, FUNCT_1:18
;
A13: F . ((F ") . o) =
(F * H) . o
by Th33
.=
o
by A12
;
dom the MorphMap of F = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;
then
[((F ") . o),((F ") . o)] in dom the MorphMap of F
by ZFMISC_1:87;
then A14:
Morph-Map (F,((F ") . o),((F ") . o)) is one-to-one
by A7;
[((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:13
.=
the Arrows of B . ((F . ((F ") . o)),(F . ((F ") . o)))
by Def10
;
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 15;
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 1
;
( the Arrows of A * the ObjectMap of (F ")) . [o,o] =
the Arrows of A . ( the ObjectMap of H . (o,o))
by A11, FUNCT_1:13
.=
the Arrows of A . (((F ") . o),((F ") . o))
by Def10
;
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 Def4;
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 15;
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 1
;
then A19:
idm o in dom (Morph-Map ((F "),o,o))
by ALTCAT_1:19;
A20: Morph-Map ((F "),o,o) =
(f "") . ( the ObjectMap of (F ") . (o,o))
by A2, A4, A11, FUNCT_1:13
.=
(f "") . [(H . o),(H . o)]
by Def10
.=
(Morph-Map (F,((F ") . o),((F ") . o))) "
by A3, A7, A8, A9, MSUALG_3:def 4
;
(Morph-Map ((F "),o,o)) . (idm o) in rng (Morph-Map ((F "),o,o))
by A19, FUNCT_1:def 3;
then A21:
(Morph-Map ((F "),o,o)) . (idm o) in dom (Morph-Map (F,((F ") . o),((F ") . o)))
by A14, A20, FUNCT_1:33;
(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:19, FUNCT_1:13
.=
(id (rng (Morph-Map (F,((F ") . o),((F ") . o))))) . (idm o)
by A14, A20, FUNCT_1:39
.=
(id (dom (Morph-Map ((F "),o,o)))) . (idm o)
by A14, A20, FUNCT_1:33
.=
idm (F . ((F ") . o))
by A13, A18
.=
(Morph-Map (F,((F ") . o),((F ") . o))) . (idm ((F ") . o))
by Def20
;
hence
(Morph-Map ((F "),o,o)) . (idm o) = idm ((F ") . o)
by A14, A16, A21; verum