let C be Category; :: thesis: for a, b being Object of C st b is terminal holds
( dom (term (a,b)) = a & cod (term (a,b)) = b )
let a, b 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) <> {} ;
hence ( dom (term (a,b)) = a & cod (term (a,b)) = b ) by CAT_1:5; :: thesis: verum