set MyBool = bool Sigma;
D0: {Sigma} c= bool Sigma by ZFMISC_1:68;
Sigma in {Sigma} by TARSKI:def 1;
then reconsider Sigma = Sigma as Element of bool Sigma by D0;
set F = (In (I,(bool REAL))) --> Sigma;
reconsider Sigma = Sigma as SigmaField of Omega ;
W2: for i being Element of In (I,(bool REAL)) holds ((In (I,(bool REAL))) --> Sigma) . i = Sigma by FUNCOP_1:7;
for i being set st i in In (I,(bool REAL)) holds
((In (I,(bool REAL))) --> Sigma) . i is SigmaField of Omega by FUNCOP_1:7;
then reconsider F = (In (I,(bool REAL))) --> Sigma as ManySortedSigmaField of In (I,(bool REAL)),Sigma by KOLMOG01:def 2;
for s, t being Element of In (I,(bool REAL)) st s <= t holds
F . s is Subset of (F . t)

proof

let s, t be Element of In (I,(bool REAL)); :: thesis:
assume s <= t ; :: thesis:
F . s = Sigma by FUNCOP_1:7;
hence F . s is Subset of (F . t) by FUNCOP_1:7; :: thesis:

end;

then F is Filtration of In (I,(bool REAL)),Sigma by Def2000;
then consider F being Filtration of In (I,(bool REAL)),Sigma such that
C0: for i being Element of In (I,(bool REAL)) holds F . i = Sigma by W2;
for j being Element of In (J,(bool REAL))
for i being Element of In (I,(bool REAL)) st j - 1 = i holds
RVProcess (Stoch,j) is_random_variable_on El_Filtration (i,F),Sigma2

proof

let j be Element of In (J,(bool REAL)); :: thesis:
let i be Element of In (I,(bool REAL)); :: thesis:
assume j - 1 = i ; :: thesis:
ex RV being Function of Omega,Omega2 st
( Stoch . j = RV & RV is_random_variable_on Sigma,Sigma2 ) by Def30000;
hence RVProcess (Stoch,j) is_random_variable_on El_Filtration (i,F),Sigma2 by C0; :: thesis:

end;

hence ex b₁ being Function of J,(set_of_random_variables_on (Sigma,Sigma2)) ex k being Filtration of In (I,(bool REAL)),Sigma st
for j being Element of In (J,(bool REAL))
for i being Element of In (I,(bool REAL)) st j - 1 = i holds
RVProcess (Stoch,j) is_random_variable_on El_Filtration (i,k),Sigma2 ; :: thesis: