theorem :: FINANCE6:17

for Omega being non empty set
for F being SigmaField of Omega
for jpi being pricefunction
for d, d2 being Nat st d > 0 & d2 = d - 1 holds
for Prob being Probability of F
for r being Real st r > - 1 holds
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )