:: deftheorem Def5000 defines RVElementsOfPortfolioValue_fut FINANCE2:def 5 :
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being sequence of X
for phi being Real_Sequence
for n being Nat
for b₇ being Function of Omega,REAL holds
( b₇ = RVElementsOfPortfolioValue_fut (phi,F,G,n) iff for w being Element of Omega holds b₇ . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );