for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for Q being ManySortedSigmaField of I,Sigma ex rv being Function of Omega,Omega2 st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2