let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for RV being random_variable of Sigma, Borel_Sets
for K being Element of REAL holds RV - (Omega --> K) is random_variable of Sigma, Borel_Sets
let Sigma be SigmaField of Omega; :: thesis: for RV being random_variable of Sigma, Borel_Sets
for K being Element of REAL holds RV - (Omega --> K) is random_variable of Sigma, Borel_Sets
let RV be random_variable of Sigma, Borel_Sets ; :: thesis: for K being Element of REAL holds RV - (Omega --> K) is random_variable of Sigma, Borel_Sets
let K be Element of REAL ; :: thesis: RV - (Omega --> K) is random_variable of Sigma, Borel_Sets
Omega --> K is random_variable of Sigma, Borel_Sets by 1A5, RANDOM_3:def 1;
hence RV - (Omega --> K) is random_variable of Sigma, Borel_Sets by FINANCE2:24; :: thesis: verum