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

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