let Omega be non empty set ; for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being Real
for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let F be SigmaField of Omega; for d being Nat st d > 0 holds
for r being Real
for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let d be Nat; ( d > 0 implies for r being Real
for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w)) )
assume A1:
d > 0
; for r being Real
for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let r be Real; for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let phi be Real_Sequence; for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
set X = set_of_random_variables_on (F,Borel_Sets);
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); ( Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) implies for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w)) )
assume A2:
Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r)
; for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let w be Element of Omega; PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
A3:
d - 1 is Element of NAT
by A1, NAT_1:20;
defpred S1[ Nat] means (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ($1 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . $1);
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0)
proof
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 1)
by SERIES_1:def 1;
then
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 1)
by SERIES_1:def 1;
then
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0) + (((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . 0)
by NAT_1:def 3;
then
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0)
by SERIES_1:def 1;
then consider d being
Element of
NAT such that A4:
(
d = 0 &
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (d + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . d) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . d) )
;
A5:
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (d + 1) = (((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . d)
by A4, Def10;
set g =
G . d;
set g2 =
Change_Element_to_Func (
F,
Borel_Sets,
(G . d));
(Change_Element_to_Func (F,Borel_Sets,(G . d))) . w = 1
+ r
proof
(
Element_Of (
F,
Borel_Sets,
G,
0)
= G . 0 &
Change_Element_to_Func (
F,
Borel_Sets,
(G . d))
= G . 0 &
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) )
by A2, Def9, Def7, A4;
hence
(Change_Element_to_Func (F,Borel_Sets,(G . d))) . w = 1
+ r
by FUNCOP_1:7;
verum
end;
hence
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0)
by A4, A5, Def8;
verum
end;
then A6:
S1[ 0 ]
;
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A8:
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (k + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)
;
S1[k + 1]
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1) = (((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . ((k + 1) + 1))
by A8, SERIES_1:def 1;
then
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1) = (((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)) + (((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (k + 1))
by NAT_1:def 3;
then
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1) = ((1 + r) * (phi . 0)) + (((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k) + (((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (k + 1)))
;
hence
S1[
k + 1]
by SERIES_1:def 1;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A6, A7);
then
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((d - 1) + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1))
by A3;
hence
PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
; verum