let C be Category; :: thesis: for c being Object of C holds (Obj (id C)) . c = c
let c be Object of C; :: thesis: (Obj (id C)) . c = c
(id C) . (id c) = id c by FUNCT_1:35;
hence (Obj (id C)) . c = c by Th103; :: thesis: verum