let C, D be Category; :: thesis: for T being Functor of C,D
for c being Object of C holds T /. (id c) = id (T . c)
let T be Functor of C,D; :: thesis: for c being Object of C holds T /. (id c) = id (T . c)
let c be Object of C; :: thesis: T /. (id c) = id (T . c)
Hom (c,c) <> {} ;
hence T /. (id c) = T . (id c) by Def10
.= id (T . c) by CAT_1:71 ;
:: thesis: verum