let Omega be non empty set ; :: thesis: ( Omega = {1,2,3,4} implies for Sigma being SigmaField of Omega
for I being non empty Subset of REAL st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets )
assume A0: Omega = {1,2,3,4} ; :: thesis: for Sigma being SigmaField of Omega
for I being non empty Subset of REAL st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets
let Sigma be SigmaField of Omega; :: thesis: for I being non empty Subset of REAL st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets
let I be non empty Subset of REAL; :: thesis: ( I = {1,2,3} & Sigma = bool {1,2,3,4} implies for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets )
assume A1: ( I = {1,2,3} & Sigma = bool {1,2,3,4} ) ; :: thesis: for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets
let MyFunc be Filtration of I,Sigma; :: thesis: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 implies for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets )
assume A2: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 ) ; :: thesis: for Prob being Probability of Sigma
for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets
let Prob be Probability of Sigma; :: thesis: for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets
let i be Element of I; :: thesis: ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets

per cases ( i = 1 or i = 2 or i = 3 ) by A1, ENUMSET1:def 1;

suppose i = 1 ; :: thesis: ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets

then consider f being Function of Omega,REAL such that
Fin1: ( f . 1 = 100 & f . 2 = 100 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets ) by A0, A2, MyFunc70;
thus ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets by Fin1; :: thesis: verum

end;

suppose i = 2 ; :: thesis: ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets

then consider f being Function of Omega,REAL such that
Fin1: ( f . 1 = 80 & f . 2 = 80 & f . 3 = 120 & f . 4 = 120 & f is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets ) by A0, A2, MyFunc60;
thus ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets by Fin1; :: thesis: verum

end;

suppose i = 3 ; :: thesis: ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets

then consider f being Function of Omega,REAL such that
Fin1: ( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 & f is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets ) by A0, A2, MyFunc50;
thus ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets by Fin1; :: thesis: verum

end;

end;