let Omega be non empty set ; 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; 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 ; 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; 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; 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; 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;
(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 S1[
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;
verum
end;
then J0:
S1[
0 ]
;
J1:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume Q0:
S1[
n]
;
S1[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
S1[
n + 1]
by SERIES_1:def 1;
verum
end;
for
n being
Nat holds
S1[
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)
;
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;
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; verum