theorem JA2: :: FINANCE6:11

for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ in F