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