:: deftheorem defines PortfolioValueFutExt FINANCE2:def 7 :
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 PortfolioValueFutExt (d,phi,F,G,w) = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d;