A constructive counterpart of the subdirect representation theorem for reduced rings

We give a constructive counterpart of the theorem of Andrunakievi{c} and Rjabuhin, which states that every reduced ring is a subdirect product of domains. As an application, we extract a constructive proof of the fact that every ring A satisfying ∀ x∈ A. x³=x is commutative from a classical proof. We also prove a similar result for semiprime ideals.