:: deftheorem Def10 defines ElementsOfPortfolioValue_fut FINANCE1:def 10 :
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for w being Element of Omega
for G being sequence of X
for phi, b₇ being Real_Sequence holds
( b₇ = ElementsOfPortfolioValue_fut (phi,F,w,G) iff for n being Element of NAT holds b₇ . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );