let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let F be SigmaField of Omega; :: thesis: for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); :: thesis: for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let phi be Real_Sequence; :: thesis: for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let d be Nat; :: thesis: RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
defpred S₁[ Nat] means RVPortfolioValueFut (phi,F,G,$1) is random_variable of F, Borel_Sets ;
ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))) is random_variable of F, Borel_Sets by FINANCE2:28;
then A1: (phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1)))) is random_variable of F, Borel_Sets by FINANCE2:26;
RVPortfolioValueFut (phi,F,G,0) is random_variable of F, Borel_Sets

proof

for w being Element of Omega holds (RVPortfolioValueFut (phi,F,G,0)) . w = ((phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))))) . w

proof

let w be Element of Omega; :: thesis: (RVPortfolioValueFut (phi,F,G,0)) . w = ((phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))))) . w
consider k being Nat such that
B0: k = 0 ;
(RVPortfolioValueFut (phi,F,G,k)) . w = PortfolioValueFut ((k + 1),phi,F,G,w) by Def4
.= ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . k by B0, SERIES_1:def 1
.= (RVPortfolioValueFutExt_El (phi,F,G,w)) . (k + 1) by NAT_1:def 3
.= (RVElementsOfPortfolioValue_fut (phi,F,G,(k + 1))) . w by FINANCE2:def 6 ;
then (RVPortfolioValueFut (phi,F,G,0)) . w = ((ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1)))) . w) * (phi . (0 + 1)) by FINANCE2:def 5, B0;
hence (RVPortfolioValueFut (phi,F,G,0)) . w = ((phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))))) . w by VALUED_1:6; :: thesis: verum

end;

hence RVPortfolioValueFut (phi,F,G,0) is random_variable of F, Borel_Sets by A1, FUNCT_2:63; :: 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 B1: S₁[n] ; :: thesis: S₁[n + 1]
C0: for w being Element of Omega holds (RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w)

proof

let w be Element of Omega; :: thesis: (RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w)
set k = n + 1;
(RVPortfolioValueFut (phi,F,G,(n + 1))) . w = PortfolioValueFut (((n + 1) + 1),phi,F,G,w) by Def4;
then (RVPortfolioValueFut (phi,F,G,(n + 1))) . w = (PortfolioValueFut ((n + 1),phi,F,G,w)) + (((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1)) by SERIES_1:def 1;
then (RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + (((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1)) by Def4
.= ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVPortfolioValueFutExt_El (phi,F,G,w)) . ((n + 1) + 1)) by NAT_1:def 3 ;
hence (RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w) by FINANCE2:def 6; :: thesis: verum

end;

K1: RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1)) is random_variable of F, Borel_Sets by FINANCE2:30;
C2: dom (RVPortfolioValueFut (phi,F,G,n)) = Omega by FUNCT_2:def 1;
dom (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) = Omega by FUNCT_2:def 1;
then ( dom (RVPortfolioValueFut (phi,F,G,(n + 1))) = (dom (RVPortfolioValueFut (phi,F,G,n))) /\ (dom (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1)))) & ( for c being object st c in dom (RVPortfolioValueFut (phi,F,G,(n + 1))) holds
(RVPortfolioValueFut (phi,F,G,(n + 1))) . c = ((RVPortfolioValueFut (phi,F,G,n)) . c) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . c) ) ) by C0, FUNCT_2:def 1, C2;
then RVPortfolioValueFut (phi,F,G,(n + 1)) = (RVPortfolioValueFut (phi,F,G,n)) + (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) by VALUED_1:def 1;
hence S₁[n + 1] by B1, K1, FINANCE2:23; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets ; :: thesis: verum