deffunc H₁( Element of NAT ) -> Element of REAL = ((ElementsOfPortfolioValueProb_fut (F,(G . $1))) . w) * (phi . $1);
ex f being Real_Sequence st
for d being Element of NAT holds f . d = H₁(d) from FUNCT_2:sch 4();
hence ex b₁ being Real_Sequence st
for n being Element of NAT holds b₁ . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ; :: thesis: verum