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:55;
hence id i in (the_hom_sets_of C) . i,i by Def3; :: thesis: verum