An assertion concerning functionally complete algebras and NP-completeness

In a paper published in J. ACM in 1990, Tobias Nipkow asserted that the problem of deciding whether or not an equation over a nontrivial functionally complete algebra has a solution is NP-complete. However, close examination of the reduction used shows that only a weaker theorem follows from his proof, namely that deciding whether or not a system of equations has a solution is NP-complete over such an algebra. Nevertheless, the statement of Nipkow is true as shown here. As a corollary of the proof we obtain that it is coNP-complete to decide whether or not an equation is an identity over a nontrivial functionally complete algebra.