let C be Category; :: thesis: for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id a = h
let a be Object of C; :: thesis: ( a is terminal implies for h being Morphism of a,a holds id a = h )
assume a is terminal ; :: 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