We have shown elsewhere how to introduce a concept of syntactic unification when terms are taken as the elements in a free
module. This is done so as to obtain an m.g.u and its uniqueness modulo isomorphism. Here we introduce the concept of an implementation: An injective function from a term algebra into another object in a different category, both free over the same denumerable
set of variables, but which carries over a generalised form of the so called Unification Axiom. We show that any implementation
induces a faithful representation of the semi-group of substitutions of a term algebra in an appropriately chosen semi-group
of homomorphisms in the target structure. We moreover show that this representation assigns unifiers to unifiers and, under
certain conditions, an m.g.u. to an m.g.u. Moreover, when the target structure for an implementation is another term algebra,
we show that a unification problem is solvable in the target if and only if it is so in the original term algebra. We qualify
these implementations as faithful. However, when the target structure is a free module of the type mentioned, we show by means of a counter-example that there
exist non-faithful implementations. We then give a necessary and sufficient condition for an implementation on one of these
modules to be faithful. Strikingly, this condition is nothing but a translation into the language of the module of the well-known
occurs-check property of usual syntactic unification. Finally we construct an example of a faithful implementation of a term
algebra in one of our free modules.