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)
proof
let s, t be Element of I; :: 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;
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
proof
let i be Element of I; :: thesis: RVProcess (Stoch,i) is El_Filtration (i,F),Sigma2 -random_variable-like
El_Filtration (i,F) = Sigma by C0;
hence RVProcess (Stoch,i) is El_Filtration (i,F),Sigma2 -random_variable-like ; :: thesis: verum
end;
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 ; :: thesis: verum