for phi being Real_Sequence
for jpi being pricefunction
for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))