let C be Category; :: thesis: for a being Object of C st a is initial holds
for h being Morphism of a,a holds id a = h
let a be Object of C; :: thesis: ( a is initial implies for h being Morphism of a,a holds id a = h )
assume a is initial ; :: thesis: for h being Morphism of a,a holds id a = h
then consider f being Morphism of a,a such that
A1: for g being Morphism of a,a holds f = g ;
let h be Morphism of a,a; :: thesis: id a = h
id a = f by A1;
hence id a = h by A1; :: thesis: verum