:: deftheorem defines ArbitrageElSigma1 FINANCE6:def 10 :
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds ArbitrageElSigma1 (phi,Omega,F,G,n) = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[;