let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being contravariant Functor of A,B
for a being object of A holds F . (idm a) = idm (F . a)
let F be contravariant 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)
thus F . (idm a) = (Morph-Map F,a,a) . (idm a) by FUNCTOR0:def 17
.= idm (F . a) by FUNCTOR0:def 21 ; :: thesis: verum