let o be object of C1; FUNCTOR0:def 21 (Morph-Map ((G * F),o,o)) . (idm o) = idm ((G * F) . o)
A1:
[o,o] in [: the carrier of C1, the carrier of C1:]
by ZFMISC_1:106;
then
[o,o] in dom the ObjectMap of F
by FUNCT_2:def 1;
then ( the Arrows of C2 * the ObjectMap of F) . [o,o] =
the Arrows of C2 . ( the ObjectMap of F . (o,o))
by FUNCT_1:23
.=
the Arrows of C2 . ((F . o),(F . o))
by Def11
.=
<^(F . o),(F . o)^>
by ALTCAT_1:def 2
;
then A2:
( the Arrows of C2 * the ObjectMap of F) . [o,o] <> {}
by ALTCAT_2:def 7;
the MorphMap of F is ManySortedFunction of the Arrows of C1, the Arrows of C2 * the ObjectMap of F
by Def5;
then
Morph-Map (F,o,o) is Function of ( the Arrows of C1 . [o,o]),(( the Arrows of C2 * the ObjectMap of F) . [o,o])
by A1, PBOOLE:def 18;
then A3: dom (Morph-Map (F,o,o)) =
the Arrows of C1 . (o,o)
by A2, FUNCT_2:def 1
.=
<^o,o^>
by ALTCAT_1:def 2
;
thus (Morph-Map ((G * F),o,o)) . (idm o) =
((Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))) . (idm o)
by Th35
.=
(Morph-Map (G,(F . o),(F . o))) . ((Morph-Map (F,o,o)) . (idm o))
by A3, ALTCAT_1:23, FUNCT_1:23
.=
(Morph-Map (G,(F . o),(F . o))) . (idm (F . o))
by Def21
.=
idm (G . (F . o))
by Def21
.=
idm ((G * F) . o)
by Th34
; verum