Seja A um conjunto não vazio, X um subconjunto de A, F um conjunto de funções em A, e o fecho indutivo de X sob F.
Seja B qualquer conjunto não vazio e seja G o conjunto de funçoes sobre o conjunto B, de forma que exista uma função em G ,que associa com cada função f de aridade n em F a seguinte função em G(G não pode ser uma bijeção).
Partindo deste lema podemos construir o conceito de Extensão Homomórfica Unica.
As identidades vistas em (1) e (2) demonstram que é um homomorfismo, chamado especificamente de Extensão Homomórfica Única de . Para provar o teorema, dois requisitos devem ser satisfeitos: provar que a extensão() existe e é única (garantindo a ausência de bijeções).
Precisamos definir uma sequencia de funções de forma indutiva , satisfazendo as condições (1) e (2) restritas a . Para isso definimos e dado então terá o seguinte grafo (lembre-se, estamos tratando um homomorfismo e portanto precisamos provar isso via grafos):
com
Primeiro devemos checar se o grafo realmente possui funcionalidade, já que é livremente gerado, pelo pequeno lema temos que quando ,então preciamos apenas determinar a funcionalidade apenas para a primeira parte da união. Tendo que os elementos de G são funções(novamente, como definido pelo lema), a unica possibilidade de ter e para algum é ter para algum e para alguns construtores e em .
Já que e são disjuntos quando isto implica que e . Sendo todo em ,nós temos que ter .
Mas então temos com , mostrando funcionalidade.
Antes de continuar precisamos utilizar um novo lema que determine regras para funções parciais, ele pode ser escrito como:
(3)Seja uma sequencia parcial de funções tal que . Então, é uma função parcial. [1]
Usando (3), é uma função parcial. Já que então é total em .
Indo além, é claro pela definição de que satisfaz (1) e (2). Para provar a unicidade de , para qualquer outra função que satifaça (1) e (2), basta usar uma indução simples que mostre que e servem para , provando assim o Teorema da Extensão Homomórfica Unica.[2]
Podemos usar o teorema da extensão no calculo numérico de expressões sobre números inteiros. Primeiramente devemos definir o seguinte:
onde
Seja
Seja o fecho indutivo de sob e seja
Seja
Então será uma função que calcula recursivamente o valor-verdade de uma proposição, e de certa forma, será uma extensão de função que associa um valor verdade a cada proposição atômica,tal que: