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 ;
hence (Obj (id C)) . c = c by Th62; :: thesis: verum