What is the proof that there is only one homomorphism from an initial object to another object?
To add on top of finrod's answer: while the existence of an initial object guarantees the uniqueness of the aforesaid morphism, the initial object's existence is not guaranteed.
As you asked this question under the functional programming tag, perhaps you meant to ask how to establish the existence of initial algebras for a given algebraic type in a functional programming language.
The existence of an initial object is not entirely trivial, but if you know some domain theory then the proof is very similar to the least fixed point theorem for continuous functions over directed CPOs.
The canonical reference eludes me right now, but brief Googling/Wikipedia dig up Abramsky's and Jung's chapter on Domain Theory (section 5, this case is the example in 5.1.3) in the Handbook of Logic in CS.