for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for phi being Real_Sequence
for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets