:: deftheorem Def5001 defines RVPortfolioValueFutExt_El FINANCE2:def 6 :
for phi being Real_Sequence
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 w being Element of Omega
for b₇ being Real_Sequence holds
( b₇ = RVPortfolioValueFutExt_El (phi,F,G,w) iff for n being Nat holds b₇ . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w );