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 )

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

hence
set_of_random_variables_on (Sigma,Borel_Sets) = Real-Valued-Random-Variables-Set Sigma
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in set_of_random_variables_on (Sigma,Borel_Sets) iff x in Real-Valued-Random-Variables-Set Sigma )

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;hereby :: thesis: ( x in Real-Valued-Random-Variables-Set Sigma implies x in set_of_random_variables_on (Sigma,Borel_Sets) )

assume
x in Real-Valued-Random-Variables-Set Sigma
; :: thesis: 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;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

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