let o be object of C1; :: according to FUNCTOR0:def 11 :: thesis: the ObjectMap of (C1 --> m) . o,o = [((C1 --> m) . o),((C1 --> m) . o)]
A1: [o,o] in [:the carrier of C1,the carrier of C1:] by ZFMISC_1:106;
<^o2,o2^> <> {} by ALTCAT_2:def 7;
then A2: the ObjectMap of (C1 --> m) . o,o = ([:the carrier of C1,the carrier of C1:] --> [o2,o2]) . [o,o] by Def18
.= [o2,o2] by A1, FUNCOP_1:13 ;
then (C1 --> m) . o = o2 by MCART_1:7;
hence the ObjectMap of (C1 --> m) . o,o = [((C1 --> m) . o),((C1 --> m) . o)] by A2; :: thesis: verum