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

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