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

proof

let i be Element of I; :: thesis: X1 is random_variable of El_Filtration (i,MyFunc),Sigma2
( i = 1 or i = 2 or i = 3 ) by A5, ENUMSET1:def 1;
hence X1 is random_variable of El_Filtration (i,MyFunc),Sigma2 by A6, A7; :: thesis: verum

end;

take {1,2,3,4} ; :: thesis: 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} ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum