I have not been able to find any formalization of random variables that supports construction of new random variables dependent on previously constructed ones. In what I have found, a random variable $A$ is a measurable function from a fixed probability space $(Ω,F,P)$ to a measurable space $(X,...