theorem :: FINANCE3:31

ex Omega, Omega2 being non empty set ex Sigma being SigmaField of Omega ex Sigma2 being SigmaField of Omega2 ex I being non empty Subset of REAL ex Q being ManySortedSigmaField of I,Sigma st
( Q is Filtration of I,Sigma & ex rv being Function of Omega,Omega2 st
for i being Element of I holds rv is random_variable of Sigma_of_ManySortedSigmaField (Q,i),Sigma2 )