:: deftheorem defines BuyPortfolioExt FINANCE1:def 3 :
for d being Nat
for phi, jpi being Real_Sequence holds BuyPortfolioExt (phi,jpi,d) = (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;