theorem
for
d being
Nat for
phi being
Real_Sequence for
Omega being non
empty set for
F being
SigmaField of
Omega for
X being non
empty set for
G being
sequence of
X for
w being
Element of
Omega holds
(
PortfolioValueFut (
(d + 1),
phi,
F,
G,
w)
= (RVPortfolioValueFut (phi,F,G,d)) . w &
{(PortfolioValueFut ((d + 1),phi,F,G,w))} is
Event of
Borel_Sets )
by Def4, FINANCE2:5;