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 = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,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
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 = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & 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 = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & 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 = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & 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 = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) )
assume A2: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 ) ; :: thesis: for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )
let eli be Element of I; :: thesis: ( eli = 1 implies ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) )
assume A4: eli = 1 ; :: thesis: ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )
125 is Element of REAL by NUMBERS:19;
hence ex f being Function of Omega,REAL st
( f . 1 = 125 & f . 2 = 125 & f . 3 = 125 & f . 4 = 125 & f is_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets ) by A0, A2, A4, MyFunc7; :: thesis: verum