set Omega = {1,2,3,4};
set Omega2 = {1};
consider Sigma being SigmaField of {1,2,3,4} such that
A3:
Sigma = bool {1,2,3,4}
;
reconsider Sigma2 = bool {1} as non empty set ;
reconsider Sigma2 = Sigma2 as SigmaField of {1} ;
consider I being non empty real-membered set such that
A5:
I = {1,2,3}
;
consider MyFunc being Filtration of I,Sigma such that
A6:
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} )
by A3, A5, MyNeed;
consider X1 being Function of {1,2,3,4},{1} such that
A7:
( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 )
by THJ1;
F2:
for i being Element of I holds X1 is random_variable of El_Filtration (i,MyFunc),Sigma2
take
{1,2,3,4}
; ex Omega2 being non empty set ex Sigma being SigmaField of {1,2,3,4} ex Sigma2 being SigmaField of Omega2 ex I being non empty real-membered set ex Q being Filtration of I,Sigma ex rv being Function of {1,2,3,4},Omega2 st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2
take
{1}
; ex Sigma being SigmaField of {1,2,3,4} ex Sigma2 being SigmaField of {1} ex I being non empty real-membered set ex Q being Filtration of I,Sigma ex rv being Function of {1,2,3,4},{1} st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2
take
Sigma
; ex Sigma2 being SigmaField of {1} ex I being non empty real-membered set ex Q being Filtration of I,Sigma ex rv being Function of {1,2,3,4},{1} st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2
take
Sigma2
; ex I being non empty real-membered set ex Q being Filtration of I,Sigma ex rv being Function of {1,2,3,4},{1} st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2
thus
ex I being non empty real-membered set ex Q being Filtration of I,Sigma ex rv being Function of {1,2,3,4},{1} st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2
by F2; verum