set MyBool = bool Sigma;
D0: {Sigma} c= bool Sigma by ZFMISC_1:68;
Sigma in {Sigma} by TARSKI:def 1;
then Sigma in bool Sigma by D0;
then reconsider Sigma = Sigma as Element of bool Sigma ;
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;
F is Filtration of In (I,(bool REAL)),Sigma

proof

WW1: 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: ( s <= t implies F . s is Subset of (F . t) )
assume s <= t ; :: thesis: F . s is Subset of (F . t)
F . s = Sigma by FUNCOP_1:7;
hence F . s is Subset of (F . t) by FUNCOP_1:7; :: thesis: verum

end;

for t being Element of In (I,(bool REAL)) holds F . t c= Sigma by FUNCOP_1:7;
hence F is Filtration of In (I,(bool REAL)),Sigma by WW1, Def2000; :: thesis: verum

end;

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: 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
let i be Element of In (I,(bool REAL)); :: thesis: ( j - 1 = i implies RVProcess (Stoch,j) is_random_variable_on El_Filtration (i,F),Sigma2 )
assume j - 1 = i ; :: thesis: RVProcess (Stoch,j) is_random_variable_on El_Filtration (i,F),Sigma2
consider RV being Function of Omega,Omega2 such that
C2: ( Stoch . j = RV & RV is_random_variable_on Sigma,Sigma2 ) by Def30000;
thus RVProcess (Stoch,j) is_random_variable_on El_Filtration (i,F),Sigma2 by C2, C0; :: thesis: verum

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: verum