We have been working on the formalization of the probability and the randomness. In  and , we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of  and . First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite probability spaces.