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 = I --> Sigma;
reconsider Sigma = Sigma as SigmaField of Omega ;
W2:
for i being Element of I holds (I --> Sigma) . i = Sigma
by FUNCOP_1:7;
for i being set st i in I holds
(I --> Sigma) . i is SigmaField of Omega
by FUNCOP_1:7;
then reconsider F = I --> Sigma as ManySortedSigmaField of I,Sigma by KOLMOG01:def 2;
WW1:
for s, t being Element of I st s <= t holds
F . s is Subset of (F . t)
F is Filtration of I,Sigma
by WW1, Def2000;
then consider F being Filtration of I,Sigma such that
C0:
for i being Element of I holds F . i = Sigma
by W2;
for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,F),Sigma2 -random_variable-like
hence
ex b1 being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) ex k being Filtration of I,Sigma st
for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,k),Sigma2 -random_variable-like
; verum