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

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