theorem Th12: :: FINANCE1:12

for Omega being non empty set
for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being Real
for phi being Real_Sequence
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
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))