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: ( 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;

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 El_Filtration (i,F),Sigma2 -random_variable-like

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 El_Filtration (i,F),Sigma2 -random_variable-like
let i be Element of In (I,(bool REAL)); :: thesis: ( j - 1 = i implies RVProcess (Stoch,j) is El_Filtration (i,F),Sigma2 -random_variable-like )
assume j - 1 = i ; :: thesis: RVProcess (Stoch,j) is El_Filtration (i,F),Sigma2 -random_variable-like
Sigma = El_Filtration (i,F) by C0;
hence RVProcess (Stoch,j) is El_Filtration (i,F),Sigma2 -random_variable-like ; :: 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 El_Filtration (i,k),Sigma2 -random_variable-like ; :: thesis: verum