ElementsOfPortfolioValueProb_fut (F,k) = Change_Element_to_Func (F,Borel_Sets,k) by FINANCE1:def 8;
hence ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets ; :: thesis: verum