defpred S₁[ Nat] means (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . $1 = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . $1;
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0 = (ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0 by SERIES_1:def 1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 0))) . w) * (phi . 0) by FINANCE1:def 10;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0 = (RVElementsOfPortfolioValue_fut (phi,F,G,0)) . w by Def5000;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0 = (RVPortfolioValueFutExt_El (phi,F,G,w)) . 0 by Def5001;
then J0: S₁[ 0 ] by SERIES_1:def 1;
J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B0: S₁[n] ; :: thesis: S₁[n + 1]
B2: (ElementsOfPortfolioValue_fut (phi,F,w,G)) . (n + 1) = (RVPortfolioValueFutExt_El (phi,F,G,w)) . (n + 1)

proof

(RVPortfolioValueFutExt_El (phi,F,G,w)) . (n + 1) = (RVElementsOfPortfolioValue_fut (phi,F,G,(n + 1))) . w by Def5001;
then (RVPortfolioValueFutExt_El (phi,F,G,w)) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . (n + 1)))) . w) * (phi . (n + 1)) by Def5000;
hence (ElementsOfPortfolioValue_fut (phi,F,w,G)) . (n + 1) = (RVPortfolioValueFutExt_El (phi,F,G,w)) . (n + 1) by FINANCE1:def 10; :: thesis: verum

end;

(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (n + 1) = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . n) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . (n + 1)) by SERIES_1:def 1, B0;
hence S₁[n + 1] by B2, SERIES_1:def 1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence ( PortfolioValueFutExt (d,phi,F,G,w) is Real & ( for b₁ being Real holds
( b₁ = PortfolioValueFutExt (d,phi,F,G,w) iff b₁ = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d ) ) ) ; :: thesis: verum