let A, B 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) <> {} ;
hence F /. (id a) = F . (id a) by CAT_3:def 10
.= id (F . a) by CAT_1:71 ;
:: thesis: verum