## Examples

Examples -> Algebra -> homomorphism.html
Explanation of homomorphism
**Theorem**: *The composition of group homomorphims is a homomorphism.*

This example illustrates that beta reduction works well with paramodulation.

The composition of two functions f and g is expressed as the lambda term lambda(x,f(g(x))).
The verification that the composition of homomorphisms is a homomorphism is a
straightforward piece of equational reasoning. However, we also need to prove
that if Phi maps G to H and Psi maps H to K then the composition maps G to K.
In this file, the groups G, H, and K are given by "propositional functions", that is,
G, H, and K are treated as constants, and "x belongs to G" is represented by Ap(G,x) = $T.
($T means "true").

This theorem illustrates how lambda logic can sometimes make it very easy to formulate
a precise version of a theorem that is rather difficult to formulate in set theory or
in a first-order algebraic theory. Wick and McCune [1] showed how to formulate and prove
this theorem in set theory. It was quite difficult.

[1] Wick, C., and McCune, W., Automated reasoning about elementary point-set topology,
*J. Automated Reasoning* **5(2)** 239-255, 1989.