:: deftheorem Def8 defines ElementsOfPortfolioValueProb_fut FINANCE1:def 8 :
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for k being Element of X
for b₅ being Function of Omega,REAL holds
( b₅ = ElementsOfPortfolioValueProb_fut (F,k) iff for w being Element of Omega holds b₅ . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w );