let C be Category; :: thesis: for a, b being Object of C holds hom (id a),(id b) = id (Hom a,b)
let a, b be Object of C; :: thesis: hom (id a),(id b) = id (Hom a,b)
thus hom (id a),(id b) = hom a,(id b) by Th53
.= id (Hom a,b) by Th43 ; :: thesis: verum