let Omega be non empty set ; :: thesis:
assume A0: Omega = {1,2,3,4} ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let I be non empty real-membered set ; :: thesis:
assume A1: ( I = {1,2,3} & Sigma = bool {1,2,3,4} ) ; :: thesis:
let MyFunc be ManySortedSigmaField of I,Sigma; :: thesis:
assume A2: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Special_SigmaField3 ) ; :: thesis:
let Prob be Function of Sigma,REAL; :: thesis:
let i be Element of I; :: thesis:

per cases by A1, ENUMSET1:def 1;

suppose a1: i = 1 ; :: thesis:

100 in REAL by NUMBERS:19;
then ex f being Function of Omega,REAL st
( 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, MyFunc7, a1;
hence ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets ; :: thesis:

end;

suppose a1: i = 2 ; :: thesis:

( 80 in REAL & 120 in REAL ) by NUMBERS:19;
then ex f being Function of Omega,REAL st
( 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, MyFunc6, a1;
hence ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets ; :: thesis:

end;

suppose a1: i = 3 ; :: thesis:

( 60 in REAL & 80 in REAL & 100 in REAL & 120 in REAL ) by NUMBERS:19;
then ex f being Function of Omega,REAL st
( 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, MyFunc5, a1;
hence ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets ; :: thesis:

end;

end;