let C be Category; :: thesis: for b, a being Object of C st b is terminal holds
( dom (term a,b) = a & cod (term a,b) = b )
let b, a be Object of C; :: thesis: ( b is terminal implies ( dom (term a,b) = a & cod (term a,b) = b ) )
assume b is terminal ; :: thesis: ( dom (term a,b) = a & cod (term a,b) = b )
then Hom a,b <> {} by CAT_1:def 15;
hence ( dom (term a,b) = a & cod (term a,b) = b ) by CAT_1:23; :: thesis: verum