for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[