let C be Category; :: thesis: for a being Object of C holds id a in Hom (a,a)
let a be Object of C; :: thesis: id a in Hom (a,a)
( dom (id a) = a & cod (id a) = a ) by Def8;
hence id a in Hom (a,a) ; :: thesis: verum