per cases ( d = 0 or d <> 0 ) ;

suppose A0: d = 0 ; :: thesis: ( PortfolioValueFut (d,phi,F,G,w) is Real & ( for b₁ being Real holds
( b₁ = PortfolioValueFut (d,phi,F,G,w) iff b₁ = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1) ) ) )

then not d - 1 in dom (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) ;
then A1: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1) = {} by FUNCT_1:def 2;
not d - 1 in dom (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) by A0;
hence ( PortfolioValueFut (d,phi,F,G,w) is Real & ( for b₁ being Real holds
( b₁ = PortfolioValueFut (d,phi,F,G,w) iff b₁ = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1) ) ) ) by A1, FUNCT_1:def 2; :: thesis: verum

end;

suppose A0: d <> 0 ; :: thesis: ( PortfolioValueFut (d,phi,F,G,w) is Real & ( for b₁ being Real holds
( b₁ = PortfolioValueFut (d,phi,F,G,w) iff b₁ = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1) ) ) )

for k being Nat holds (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . k

proof

let k be Nat; :: thesis: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . k
defpred S₁[ Nat] means (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . $1 = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . $1;
consider k being Nat such that
B0: k = 0 ;
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . k by B0, SERIES_1:def 1;
then B1: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k = (ElementsOfPortfolioValue_fut (phi,F,w,G)) . (k + 1) by NAT_1:def 3;
(Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . k = ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . k by B0, SERIES_1:def 1
.= (RVPortfolioValueFutExt_El (phi,F,G,w)) . (k + 1) by NAT_1:def 3
.= (RVElementsOfPortfolioValue_fut (phi,F,G,(k + 1))) . w by FINANCE2:def 6 ;
then (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . k = ((ElementsOfPortfolioValueProb_fut (F,(G . (k + 1)))) . w) * (phi . (k + 1)) by FINANCE2:def 5;
then J0: S₁[ 0 ] by FINANCE1:def 10, B1, B0;
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 C0: S₁[n] ; :: thesis: S₁[n + 1]
((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (phi,F,w,G)) . ((n + 1) + 1) by NAT_1:def 3
.= ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . w) * (phi . ((n + 1) + 1)) by FINANCE1:def 10
.= (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w by FINANCE2:def 5
.= (RVPortfolioValueFutExt_El (phi,F,G,w)) . ((n + 1) + 1) by FINANCE2:def 6 ;
then ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (n + 1) = ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1) by NAT_1:def 3;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (n + 1) = ((Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . n) + (((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1)) by SERIES_1:def 1, C0
.= (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (n + 1) by SERIES_1:def 1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . k ; :: thesis: verum

end;

hence ( PortfolioValueFut (d,phi,F,G,w) is Real & ( for b₁ being Real holds
( b₁ = PortfolioValueFut (d,phi,F,G,w) iff b₁ = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1) ) ) ) by A0; :: thesis: verum

end;

end;