let Omega be non empty set ; for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds
( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )
let Sigma be SigmaField of Omega; for f being Function of Omega,REAL holds
( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )
let f be Function of Omega,REAL; ( f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma )
thus
( f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma )
by FINANCE1:15; ( f is Real-Valued-Random-Variable of Sigma implies f is Sigma, Borel_Sets -random_variable-like )
assume A1:
f is Real-Valued-Random-Variable of Sigma
; f is Sigma, Borel_Sets -random_variable-like
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
hence
f is Sigma, Borel_Sets -random_variable-like
; verum