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

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