let C be Category; :: thesis: for a being Object of C holds (id a) * (id a) = id a
let a be Object of C; :: thesis: (id a) * (id a) = id a
Hom (a,a) <> {} by Th55;
hence (id a) * (id a) = id a by Th57; :: thesis: verum