let phi be Real_Sequence; :: thesis: for jpi being pricefunction
for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
let jpi be pricefunction ; :: thesis: for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
let d be Nat; :: thesis: ( d > 0 implies BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) )
assume d > 0 ; :: thesis: BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
then A1: d - 1 is Element of NAT by NAT_1:20;
defpred S₁[ Nat] means (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ($1 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . $1);
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0)

proof

(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . 0) + ((ElementsOfBuyPortfolio (phi,jpi)) . 1) by SERIES_1:def 1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((ElementsOfBuyPortfolio (phi,jpi)) . 0) + ((ElementsOfBuyPortfolio (phi,jpi)) . 1) by SERIES_1:def 1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((ElementsOfBuyPortfolio (phi,jpi)) . 0) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . 0) by NAT_1:def 3;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((ElementsOfBuyPortfolio (phi,jpi)) . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) by SERIES_1:def 1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((phi . 0) * (jpi . 0)) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) by VALUED_1:5;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((phi . 0) * 1) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) by Def2;
hence (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) ; :: thesis: verum

end;

then A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (k + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 12;
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1) = ((phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k)) + ((ElementsOfBuyPortfolio (phi,jpi)) . ((k + 1) + 1)) by A4, SERIES_1:def 1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1) = ((phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k)) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (k + 1)) by NAT_1:def 3;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1) = (phi . 0) + (((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (k + 1))) ;
hence S₁[k + 1] by SERIES_1:def 1; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((d - 1) + 1) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) by A1;
hence BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) ; :: thesis: verum