theorem :: FINANCE3:38

for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for Prob being Function of Sigma,REAL
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets