let C, D be Category; :: thesis: for T being Functor of C,D
for c being Object of C holds T . (id c) = id ((Obj T) . c)
let T be Functor of C,D; :: thesis: for c being Object of C holds T . (id c) = id ((Obj T) . c)
let c be Object of C; :: thesis: T . (id c) = id ((Obj T) . c)
ex d being Object of D st T . (id c) = id d by Def19;
hence T . (id c) = id ((Obj T) . c) by Th62; :: thesis: verum