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
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) )
assume A1: Omega = {1,2,3,4} ; :: thesis: for Sigma being SigmaField of Omega
for I being non empty Subset of REAL
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )
let Sigma be SigmaField of Omega; :: thesis: for I being non empty Subset of REAL
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )
let I be non empty Subset of REAL; :: thesis: for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 holds
for eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,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 eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) )
assume A3: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 ) ; :: thesis: for eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )
let eli be Element of I; :: thesis: ( eli = 2 implies ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) )
assume A4: eli = 2 ; :: thesis: ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )
( 150 is Element of REAL & 100 is Element of REAL ) by NUMBERS:19;
then consider f being Function of Omega,REAL such that
A5: ( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) by A1, A3, A4, MyFunc6;
thus ex f being Function of Omega,REAL st
( f . 1 = 150 & f . 2 = 150 & f . 3 = 100 & f . 4 = 100 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) by A5; :: thesis: verum