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 holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))