:: deftheorem Def4 defines RVPortfolioValueFut FINANCE3:def 3 :
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 d being Nat
for b₇ being Function of Omega,REAL holds
( b₇ = RVPortfolioValueFut (phi,F,G,d) iff for w being Element of Omega holds b₇ . w = PortfolioValueFut ((d + 1),phi,F,G,w) );