let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma
let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL holds set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma
let f be Function of Omega,REAL; :: thesis: set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma
for x being object holds
( x in set_of_random_variables_on (Sigma,Borel_Sets) iff x in Real-Valued-Random-Variables-Set Sigma )

proof

let x be object ; :: thesis: ( x in set_of_random_variables_on (Sigma,Borel_Sets) iff x in Real-Valued-Random-Variables-Set Sigma )

hereby :: thesis: ( x in Real-Valued-Random-Variables-Set Sigma implies x in set_of_random_variables_on (Sigma,Borel_Sets) )

assume x in set_of_random_variables_on (Sigma,Borel_Sets) ; :: thesis: x in Real-Valued-Random-Variables-Set Sigma
then consider f being Function of Omega,REAL such that
A1: ( x = f & f is Sigma, Borel_Sets -random_variable-like ) ;
( f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma ) by Th7;
hence x in Real-Valued-Random-Variables-Set Sigma by A1; :: thesis: verum

end;

assume x in Real-Valued-Random-Variables-Set Sigma ; :: thesis: x in set_of_random_variables_on (Sigma,Borel_Sets)
then consider q being Real-Valued-Random-Variable of Sigma such that
A2: x = q ;
q is Sigma, Borel_Sets -random_variable-like by Th7;
hence x in set_of_random_variables_on (Sigma,Borel_Sets) by A2; :: thesis: verum

end;

hence set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma by TARSKI:2; :: thesis: verum