for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real holds (Omega --> K) - RV is random_variable of F, Borel_Sets