let C be Category; :: thesis: for i being Object of C holds id i in (the_hom_sets_of C) . (i,i)
let i be Object of C; :: thesis: id i in (the_hom_sets_of C) . (i,i)
id i in Hom (i,i) by CAT_1:27;
hence id i in (the_hom_sets_of C) . (i,i) by Def3; :: thesis: verum