Suppose there are two functions:
$ f : X \rightarrow Y $ and $g : Y \rightarrow Z$
Both $g$ and $f$ can be implemented as algorithms that yield the correct result in a finite amount of time.
It appears to be obvious, that there is also a correct and terminating algorithm that computes the composition of the two $g \circ f$.
But why is that so? Do I need to argue that for both functions, there is a representation in the lambda calculus and in that calculus (with a small-step semantics), there is a trivial implementation of $\circ$? Doesn't that require an encoding of $X$,$Y$ and $Z$? Is there a more fundamental theorem?