let o be object of C1; :: according to FUNCTOR0:def 21 :: 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: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 ; :: thesis: verum