theorem :: FINANCE3:30
ex Omega, Omega2 being non empty set ex Sigma being SigmaField of Omega ex Sigma2 being SigmaField of Omega2 ex I being non empty real-membered set ex Q being Filtration 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