let C be non empty with_identities CategoryStr ; :: 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