for Omega being non empty set
for F being SigmaField of Omega
for k being Element of set_of_random_variables_on (F,Borel_Sets) holds ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets