consider MyFunc being Filtration of I,Sigma such that
B1: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} ) by A0000, A00, A000, MyNeed;
per cases ( i = 2 or i <> 2 ) ;
suppose SUPP: i = 2 ; :: thesis: ( ( i = 2 implies f2 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( not i = 2 implies f1 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b1 being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) )
( 80 in REAL & 120 in REAL ) by NUMBERS:19;
then consider f being Function of Omega,REAL such that
B4: ( f . 1 = 80 & f . 2 = 80 & f . 3 = 120 & f . 4 = 120 & f is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ) by A000, B1, MyFunc6, SUPP;
f is Sigma, Borel_Sets -random_variable-like by A00;
then ZW1: f in set_of_random_variables_on (Sigma,Borel_Sets) ;
dom f = Omega by FUNCT_2:def 1;
then KK: dom f = dom f2 by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = f2 . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = f2 . x )
assume x in dom f ; :: thesis: f . x = f2 . x
then reconsider x = x as Element of Omega ;
( x = 1 or x = 2 or x = 3 or x = 4 ) by A000, ENUMSET1:def 2;
hence f . x = f2 . x by B4, A1; :: thesis: verum
end;
hence ( ( i = 2 implies f2 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( not i = 2 implies f1 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b1 being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) ) by ZW1, SUPP, FUNCT_1:2, KK; :: thesis: verum
end;
suppose F1: i <> 2 ; :: thesis: ( ( i = 2 implies f2 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( not i = 2 implies f1 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b1 being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) )
( 60 in REAL & 80 in REAL & 100 in REAL & 120 in REAL ) by NUMBERS:19;
then consider f being Function of Omega,REAL such that
B4: ( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 & f is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ) by A000, B1, MyFunc5, MyI, F1;
f is Sigma, Borel_Sets -random_variable-like by A00;
then ZW1: f in set_of_random_variables_on (Sigma,Borel_Sets) ;
dom f = Omega by FUNCT_2:def 1;
then KK: dom f = dom f1 by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = f1 . x
proof
let x be object ; :: thesis: ( x in dom f implies f . x = f1 . x )
assume x in dom f ; :: thesis: f . x = f1 . x
then reconsider x = x as Element of Omega ;
( x = 1 or x = 2 or x = 3 or x = 4 ) by A000, ENUMSET1:def 2;
hence f . x = f1 . x by B4, A0; :: thesis: verum
end;
hence ( ( i = 2 implies f2 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( not i = 2 implies f1 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b1 being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) ) by ZW1, F1, KK, FUNCT_1:2; :: thesis: verum
end;
end;