let o1 be Object of C1; :: according to FUNCTOR0:def 20 :: thesis: (Morph-Map ((C1 --> (idm o2)),o1,o1)) . (idm o1) = idm ((C1 --> (idm o2)) . o1)
A1: <^o2,o2^> <> {} by ALTCAT_2:def 7;
<^o1,o1^> <> {} by ALTCAT_2:def 7;
hence (Morph-Map ((C1 --> (idm o2)),o1,o1)) . (idm o1) = idm o2 by A1, Th24
.= idm ((C1 --> (idm o2)) . o1) by A1, Th21 ;
:: thesis: verum