let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being covariant Functor of A,B
for a being Object of A holds F . (idm a) = idm (F . a)
let F be covariant Functor of A,B; :: thesis: for a being Object of A holds F . (idm a) = idm (F . a)
let a be Object of A; :: thesis: F . (idm a) = idm (F . a)
( <^a,a^> <> {} & <^(F . a),(F . a)^> <> {} ) by ALTCAT_2:def 7;
hence F . (idm a) = (Morph-Map (F,a,a)) . (idm a) by FUNCTOR0:def 15
.= idm (F . a) by FUNCTOR0:def 20 ;
:: thesis: verum