let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for X being non empty set
for G being sequence of X
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))
let F be SigmaField of Omega; :: thesis: for X being non empty set
for G being sequence of X
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))
let X be non empty set ; :: thesis: for G being sequence of X
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))
let G be sequence of X; :: thesis: for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))
let phi be Real_Sequence; :: thesis: for d being Nat holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))
let d be Nat; :: thesis: RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))
C0: for w being Element of Omega holds (RVPortfolioValueFutExt (phi,F,G,(d + 1))) . w = ((RVPortfolioValueFut (phi,F,G,d)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,0)) . w)

proof

let w be Element of Omega; :: thesis: (RVPortfolioValueFutExt (phi,F,G,(d + 1))) . w = ((RVPortfolioValueFut (phi,F,G,d)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,0)) . w)
A01: (RVPortfolioValueFut (phi,F,G,d)) . w = PortfolioValueFut ((d + 1),phi,F,G,w) by Def4;
for d being Nat holds (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . d = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (d + 1)) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0)

proof

defpred S₁[ Nat] means (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . $1 = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . ($1 + 1)) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0);
B1: (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . 0 = ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . 0 by SERIES_1:def 1;
(Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . 0 = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (0 + 1)) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0)

proof

(Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (0 + 1) = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . 0) + ((RVPortfolioValueFutExt_El (phi,F,G,w)) . (0 + 1)) by SERIES_1:def 1;
then (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . 0 = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (0 + 1)) - ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . 0) by NAT_1:def 3, B1;
hence (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . 0 = ((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (0 + 1)) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0) by SERIES_1:def 1; :: thesis: verum

end;

then J0: S₁[ 0 ] ;
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 Q0: S₁[n] ; :: thesis: S₁[n + 1]
(Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 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
.= (((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (n + 1)) + (((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1))) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0) by Q0
.= (((Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . (n + 1)) + ((RVPortfolioValueFutExt_El (phi,F,G,w)) . ((n + 1) + 1))) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0) by NAT_1:def 3 ;
hence S₁[n + 1] by SERIES_1:def 1; :: thesis: verum

end;

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

end;

then (RVPortfolioValueFut (phi,F,G,d)) . w = (PortfolioValueFutExt ((d + 1),phi,F,G,w)) - ((RVPortfolioValueFutExt_El (phi,F,G,w)) . 0) by A01
.= (PortfolioValueFutExt ((d + 1),phi,F,G,w)) - ((RVElementsOfPortfolioValue_fut (phi,F,G,0)) . w) by FINANCE2:def 6 ;
hence (RVPortfolioValueFutExt (phi,F,G,(d + 1))) . w = ((RVPortfolioValueFut (phi,F,G,d)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,0)) . w) by Def2; :: thesis: verum

end;

C2: dom (RVPortfolioValueFut (phi,F,G,d)) = Omega by FUNCT_2:def 1;
dom (RVElementsOfPortfolioValue_fut (phi,F,G,0)) = Omega by FUNCT_2:def 1;
then ( dom (RVPortfolioValueFutExt (phi,F,G,(d + 1))) = (dom (RVPortfolioValueFut (phi,F,G,d))) /\ (dom (RVElementsOfPortfolioValue_fut (phi,F,G,0))) & ( for c being object st c in dom (RVPortfolioValueFutExt (phi,F,G,(d + 1))) holds
(RVPortfolioValueFutExt (phi,F,G,(d + 1))) . c = ((RVPortfolioValueFut (phi,F,G,d)) . c) + ((RVElementsOfPortfolioValue_fut (phi,F,G,0)) . c) ) ) by C0, FUNCT_2:def 1, C2;
hence RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0)) by VALUED_1:def 1; :: thesis: verum