let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds
( f is_random_variable_on Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma )
let Sigma be SigmaField of Omega; :: thesis: for f being Function of Omega,REAL holds
( f is_random_variable_on Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma )
let f be Function of Omega,REAL; :: thesis: ( f is_random_variable_on Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma )
thus ( f is_random_variable_on Sigma, Borel_Sets implies f is Real-Valued-Random-Variable of Sigma ) by FINANCE1:15; :: thesis: ( f is Real-Valued-Random-Variable of Sigma implies f is_random_variable_on Sigma, Borel_Sets )
assume A1: f is Real-Valued-Random-Variable of Sigma ; :: thesis: f is_random_variable_on Sigma, Borel_Sets
set B = { x where x is Element of Borel_Sets : f " x is Element of Sigma } ;
A2: { x where x is Element of Borel_Sets : f " x is Element of Sigma } = Borel_Sets by Th6, A1;
for x being set st x in Borel_Sets holds
f " x in Sigma

proof

let x be set ; :: thesis: ( x in Borel_Sets implies f " x in Sigma )
assume x in Borel_Sets ; :: thesis: f " x in Sigma
then ex z being Element of Borel_Sets st
( z = x & f " z is Element of Sigma ) by A2;
hence f " x in Sigma ; :: thesis: verum

end;

hence f is_random_variable_on Sigma, Borel_Sets ; :: thesis: verum