let Omega be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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 S₁[ 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; :: thesis: 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; :: thesis: verum

end;

then A6: S₁[ 0 ] ;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[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) ; :: thesis: S₁[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 S₁[k + 1] by SERIES_1:def 1; :: thesis: verum

end;

for k being Nat holds S₁[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)) ; :: thesis: verum