for Omega, Omega2 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 Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
ex Stoch being Stochastic_Process of I,Sigma, Borel_Sets st
( ( for k being Element of I holds
( ex RV being Function of Omega,REAL st
( Stoch . k = RV & RV is Sigma, Borel_Sets -random_variable-like & RV is El_Filtration (k,MyFunc), Borel_Sets -random_variable-like ) & ex f being Function of Omega,REAL st
( k = 1 implies ( f . 1 = 100 & f . 2 = 100 & f . 3 = 100 & f . 4 = 100 & Stoch . k = f ) ) & ex f being Function of Omega,REAL st
( k = 2 implies ( f . 1 = 80 & f . 2 = 80 & f . 3 = 120 & f . 4 = 120 & Stoch . k = f ) ) & ex f being Function of Omega,REAL st
( k = 3 implies ( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 & Stoch . k = f ) ) & Stoch is MyFunc -stoch_proc_wrt_to_Filtration ) ) & Stoch is Adapted_Stochastic_Process of Stoch )