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