per cases ( ( not i = 2 & not i = 3 ) or i = 2 or i = 3 ) ;

suppose F1: ( not i = 2 & not i = 3 ) ; :: thesis: ( ( ( i = 2 or i = 3 ) implies FunctionRV1 (i,Sigma,f1,f2,f3) is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( i = 2 or i = 3 or f3 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b₁ being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) )

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;
B3: i = 1 by F1, A0000, ENUMSET1:def 1;
100 in REAL by NUMBERS:19;
then consider f being Function of Omega,REAL such that
B4: ( f . 1 = 100 & f . 2 = 100 & f . 3 = 100 & f . 4 = 100 & f is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like ) by A000, B1, B3, MyFunc7;
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 f3 by FUNCT_2:def 1;
for x being object st x in dom f holds
f . x = f3 . x

proof

let x be object ; :: thesis: ( x in dom f implies f . x = f3 . x )
assume x in dom f ; :: thesis: f . x = f3 . 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 = f3 . x by B4, A2; :: thesis: verum

end;

hence ( ( ( i = 2 or i = 3 ) implies FunctionRV1 (i,Sigma,f1,f2,f3) is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( i = 2 or i = 3 or f3 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b₁ being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) ) by KK, ZW1, FUNCT_1:2; :: thesis: verum

end;

suppose ( i = 2 or i = 3 ) ; :: thesis: ( ( ( i = 2 or i = 3 ) implies FunctionRV1 (i,Sigma,f1,f2,f3) is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( i = 2 or i = 3 or f3 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b₁ being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) )

hence ( ( ( i = 2 or i = 3 ) implies FunctionRV1 (i,Sigma,f1,f2,f3) is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( i = 2 or i = 3 or f3 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( for b₁ being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum ) ) ; :: thesis: verum

end;

end;