let o be object of C1; FUNCTOR0:def 11 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; verum