let a be Object of C; :: 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 ;
hence id a is invertible ; :: thesis: verum