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 Th52
.= id (Hom (a,b)) by Th42 ; :: thesis: verum