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 16
.= idm (F . a) by FUNCTOR0:def 20 ; :: thesis: verum