let o be Object of C1; :: according to FUNCTOR0:def 10 :: 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:87;
<^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 Def17
.= [o2,o2] by A1, FUNCOP_1:7 ;
thus the ObjectMap of (C1 --> m) . (o,o) = [((C1 --> m) . o),((C1 --> m) . o)] by A2; :: thesis: verum