theorem :: FINANCE3:47

for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty Subset of REAL
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )