theorem JC1: :: FINANCE6:14

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