theorem JB1: :: FINANCE6:11

for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for n being Nat
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 : PortfolioValueFutExt (n,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[