:: deftheorem defines PortfolioValueFut FINANCE3:def 2 :
for d being Nat
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 holds PortfolioValueFut (d,phi,F,G,w) = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1);