:: deftheorem Def2 defines RVPortfolioValueFutExt FINANCE3:def 1 :
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₇ = RVPortfolioValueFutExt (phi,F,G,d) iff for w being Element of Omega holds b₇ . w = PortfolioValueFutExt (d,phi,F,G,w) );