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 = Trivial-SigmaField {1,2,3,4} ) ; :: 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 El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ) by A0, A2, MyFunc7, a1;
hence ex RV being Function of Omega,REAL st RV is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ; :: 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 El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ) by A0, A2, MyFunc6, a1;
hence ex RV being Function of Omega,REAL st RV is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ; :: 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 El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ) by A0, A2, MyFunc5, a1;
hence ex RV being Function of Omega,REAL st RV is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ; :: thesis:

end;

end;