The identities seen in (1) e (2) show that \hat h is an homomorphism, specifically named the
unique homomorphic extension of h. To prove the theorem, two requirements must be met: to prove that the extension (\hat h) exists and is unique (assuring the lack of bijections).
Proof of the theorem We must define a sequence of functions h_i:X_i\to B inductively, satisfying conditions (1) and (2) restricted to X_i. For this, we define h_0=h, and given h_i then h_{i+1}shall have the following graph: : {\{(f(x_1,\ldots,x_n),g(h_i(x_1),\ldots,h_i(x_n))) \mid (x_1,\ldots,x_n)\in X^n_i - X^n_{i-1},f\in F\}} \cup {\operatorname{graph}(h_i)} \text{ with } g=d(f) First we must be certain the graph actually has functionality, since X_+ is a free set, from the lemma we have f(x_1,\ldots,x_n)\in X_{i+1} - X_i when (x_1,\ldots,x_n)\in X^n_i - X^n_{i-1},(i\geq 0), so we only have to determine the functionality for the left side of the union. Knowing that the elements of
G are functions(again, as defined by the lemma), the only instance where (x,y)\in graph(h_i) and (x,z)\in graph(h_i) for some x\in X_{i+1} - X_i is possible is if we have x=f(x_1,\ldots,x_m)=f'(y_1,\ldots,y_n) for some (x_1,\ldots,x_m)\in X^m_i - X^m_{i-1},(y_1,\ldots,y_n)\in X^n_i - X^n_{i-1} and for some generators f and {f'} in F. Since f(X^m_+) and {f'}(X^n_+) are disjoint when f\neq {f'},f(x_1,\ldots,x_m) = f'(y_1,\ldots,Y_n) this implies f=f' and m=n. Being all f\in F in X^n_+, we must have x_j=y_j,\forall j,1\leq j\leq n. Then we have y=z=g(x_1,\ldots,x_n) with g=d(f) , displaying functionality. Before moving further we must make use of a new lemma that determines the rules for partial functions, it may be written as: (3)Be (f_n)_{n\geq 0} a sequence of partial functions f_n:A\to B such that f_n\subseteq f_{n+1},\forall n\geq 0. Then, g=(A,\bigcup graph(f_n),B) is a
partial function. Using (3), \hat h =\bigcup_{i\geq 0} h_i is a partial function. Since dom(\hat h)=\bigcup dom(h_i)=\bigcup X_i=X_+ then \hat h is total in X_+. Furthermore, it is clear from the definition of h_i that \hat h satisfies (1) and (2). To prove the uniqueness of \hat h, or any other function {h'} that satisfies (1) and (2), it is enough to use a simple induction that shows \hat h and {h'} work for X_i,\forall i\geq 0, and such is proved the Theorem of the Unique Homomorphic Extension.[http://phil.gu.se/logic/books/Gallier:Logic_For_Computer_Science.pdf == Example of a particular case ==