ElementsOfBuyPortfolio (phi,jpi) = phi (#) jpi ;
hence ElementsOfBuyPortfolio (phi,jpi) is Real_Sequence ; :: thesis: verum