let o be Object of C1; :: according to FUNCTOR0:def 20 :: thesis: (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:87;
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:13
.= the Arrows of C2 . ((F . o),(F . o)) by Def10
.= <^(F . o),(F . o)^> by ALTCAT_1:def 1 ;
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 Def4;
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 15;
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 1 ;
thus (Morph-Map ((G * F),o,o)) . (idm o) = ((Morph-Map (G,(F . o),(F . o))) * (Morph-Map (F,o,o))) . (idm o) by Th34
.= (Morph-Map (G,(F . o),(F . o))) . ((Morph-Map (F,o,o)) . (idm o)) by A3, ALTCAT_1:19, FUNCT_1:13
.= (Morph-Map (G,(F . o),(F . o))) . (idm (F . o)) by Def20
.= idm (G . (F . o)) by Def20
.= idm ((G * F) . o) by Th33 ; :: thesis: verum