let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for d being natural number st d > 0 holds
for r being real number
for phi being Real_Sequence
for G being Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
let F be SigmaField of Omega; :: thesis: for d being natural number st d > 0 holds
for r being real number
for phi being Real_Sequence
for G being Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
let d be natural number ; :: thesis: ( d > 0 implies for r being real number
for phi being Real_Sequence
for G being Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w)) )
assume A0: d > 0 ; :: thesis: for r being real number
for phi being Real_Sequence
for G being Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
let r be real number ; :: thesis: for phi being Real_Sequence
for G being Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
let phi be Real_Sequence; :: thesis: for G being Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
set X = set_of_random_variables_on (F,Borel_Sets);
let G be Function of NAT,(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 (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w)) )
assume A3: Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ; :: thesis: for w being Element of Omega holds PortfolioValueFutExt (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
let w be Element of Omega; :: thesis: PortfolioValueFutExt (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
A4: d - 1 is Element of NAT by A0, NAT_1:20;
defpred S₁[ Nat] means (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . ($1 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . $1);
(Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (0 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . 0)

proof

(Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (0 + 1) = ((Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . 0) + ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . 1) by SERIES_1:def 1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . 0) + ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . 1) by SERIES_1:def 1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . 0) + (((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1) . 0) by NAT_1:def 3;
then (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . 0) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . 0) by SERIES_1:def 1;
then consider d being Element of NAT such that
AJ0: ( d = 0 & (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (d + 1) = ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . d) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . d) ) ;
AJ1: (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (d + 1) = (((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . d) by AJ0, Def14;
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 A3, Def13, Def10, AJ0;
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 (r,phi,F,w,G))) . (0 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . 0) by AJ0, AJ1, Def11; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume T0: (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . (k + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,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 (r,phi,F,w,G))) . ((k + 1) + 1) = (((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . k)) + ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) . ((k + 1) + 1)) by T0, SERIES_1:def 1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . ((k + 1) + 1) = (((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . k)) + (((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1) . (k + 1)) by NAT_1:def 3;
then (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . ((k + 1) + 1) = ((1 + r) * (phi . 0)) + (((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . k) + (((ElementsOfPortfolioValue_fut (r,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(TT0, TT1);
then (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . ((d - 1) + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . (d - 1)) by A4;
hence PortfolioValueFutExt (r,d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w)) ; :: thesis: verum