let B, A be Category; :: thesis: for F being Functor of A,B
for a being Object of A holds F . (id a) = id (F . a)
let F be Functor of A,B; :: thesis: for a being Object of A holds F . (id a) = id (F . a)
let a be Object of A; :: thesis: F . (id a) = id (F . a)
Hom (a,a) <> {} by CAT_1:56;
hence F . (id a) = F . (id a) by Def1
.= id (F . a) by CAT_1:108 ;
:: thesis: verum