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_{1}[ 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)_{1}[ 0 ]
;

A3: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[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

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

(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0)

proof

then A2:
S
(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 (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

A3: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (k + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) ; :: thesis: S_{1}[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_{1}[k + 1]
by SERIES_1:def 1; :: thesis: verum

end;assume A4: (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (k + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) ; :: thesis: S

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

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