let A, B be non empty transitive with_units AltCatStr ; for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive & F is Covariant holds
for o1, o2 being Object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
let F be reflexive feasible FunctorStr over A,B; ( F is bijective & F is coreflexive & F is Covariant implies for o1, o2 being Object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m )
assume A1:
( F is bijective & F is coreflexive & F is Covariant )
; for o1, o2 being Object of B
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
set G = F " ;
A2:
F " is Covariant
by A1, Th38;
reconsider H = F " as reflexive feasible FunctorStr over B,A by A1, Th35, Th36;
A3:
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
A4:
f = the MorphMap of F
and
A5:
the MorphMap of (F ") = (f "") * ( the ObjectMap of F ")
by A1, Def38;
F is injective
by A1;
then
F is faithful
;
then A6:
the MorphMap of F is "1-1"
;
F is surjective
by A1;
then
F is full
;
then A7:
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" )
;
let o1, o2 be Object of B; for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
(Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
let m be Morphism of o1,o2; ( <^o1,o2^> <> {} implies (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m )
assume A8:
<^o1,o2^> <> {}
; (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) = m
A9:
[((F ") . o1),((F ") . o2)] in [: the carrier of A, the carrier of A:]
by ZFMISC_1:87;
A10:
[o1,o2] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
then A11:
[o1,o2] in dom the ObjectMap of (F ")
by FUNCT_2:def 1;
dom the MorphMap of F = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;
then
[((F ") . o1),((F ") . o2)] in dom the MorphMap of F
by ZFMISC_1:87;
then A12:
Morph-Map (F,((F ") . o1),((F ") . o2)) is one-to-one
by A6;
( the Arrows of A * the ObjectMap of (F ")) . [o1,o2] =
the Arrows of A . ( the ObjectMap of H . (o1,o2))
by A11, FUNCT_1:13
.=
the Arrows of A . ((H . o1),(H . o2))
by A2, Th22
.=
<^(H . o1),(H . o2)^>
by ALTCAT_1:def 1
;
then A13:
( the Arrows of A * the ObjectMap of (F ")) . [o1,o2] <> {}
by A2, A8, Def18;
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 "),o1,o2) is Function of ( the Arrows of B . [o1,o2]),(( the Arrows of A * the ObjectMap of (F ")) . [o1,o2])
by A10, PBOOLE:def 15;
then A14: dom (Morph-Map ((F "),o1,o2)) =
the Arrows of B . (o1,o2)
by A13, FUNCT_2:def 1
.=
<^o1,o2^>
by ALTCAT_1:def 1
;
A15: Morph-Map ((F "),o1,o2) =
(f "") . ( the ObjectMap of (F ") . (o1,o2))
by A3, A5, A11, FUNCT_1:13
.=
(f "") . [(H . o1),(H . o2)]
by A2, Th22
.=
(Morph-Map (F,((F ") . o1),((F ") . o2))) "
by A4, A6, A7, A9, MSUALG_3:def 4
;
thus (Morph-Map (F,((F ") . o1),((F ") . o2))) . ((Morph-Map ((F "),o1,o2)) . m) =
((Morph-Map (F,((F ") . o1),((F ") . o2))) * (Morph-Map ((F "),o1,o2))) . m
by A8, A14, FUNCT_1:13
.=
(id (rng (Morph-Map (F,((F ") . o1),((F ") . o2))))) . m
by A12, A15, FUNCT_1:39
.=
(id (dom (Morph-Map ((F "),o1,o2)))) . m
by A12, A15, FUNCT_1:33
.=
m
by A14
; verum