let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for k being Element of set_of_random_variables_on (F,Borel_Sets) holds ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets
let F be SigmaField of Omega; :: thesis: for k being Element of set_of_random_variables_on (F,Borel_Sets) holds ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets
let k be Element of set_of_random_variables_on (F,Borel_Sets); :: thesis: ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets
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 by T; :: thesis: verum