A2: not C is empty by A1;
A3: id- a = a by CAT_6:def 20;
then id- a |> id- a by A2, CAT_6:23;
then id- a in Hom (a,a) by A3;
hence id- a is Morphism of a,a by Def3; :: thesis: verum