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