let C be Category; :: thesis: for a being Object of C holds a,a are_isomorphic
let a be Object of C; :: thesis: a,a are_isomorphic
thus A1: Hom (a,a) <> {} by Th55; :: according to CAT_1:def 14 :: thesis: ex f being Morphism of a,a st f is invertible
take id a ; :: thesis: id a is invertible
(id a) * (id a) = id a by Th59;
hence id a is invertible by A1, Th70; :: thesis: verum