let B, A be Category; :: thesis: for F being Functor of A,B
for a being Object of A holds (id F) . a = id (F . a)
let F be Functor of A,B; :: thesis: for a being Object of A holds (id F) . a = id (F . a)
let a be Object of A; :: thesis: (id F) . a = id (F . a)
thus (id F) . a = (id F) . a by Def5
.= id (F . a) by Def4 ; :: thesis: verum