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