let Omega be non empty set ; 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 n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
let F be SigmaField of Omega; for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for phi being Real_Sequence
for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); for phi being Real_Sequence
for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
let phi be Real_Sequence; for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
let n be Nat; RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
ElementsOfPortfolioValueProb_fut (F,(G . n)) is random_variable of F, Borel_Sets
by T1;
then A1:
(phi . n) (#) (ElementsOfPortfolioValueProb_fut (F,(G . n))) is random_variable of F, Borel_Sets
by Th8;
for w being Element of Omega holds ((phi . n) (#) (ElementsOfPortfolioValueProb_fut (F,(G . n)))) . w = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
proof
let w be
Element of
Omega;
((phi . n) (#) (ElementsOfPortfolioValueProb_fut (F,(G . n)))) . w = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
(phi . n) * ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) = ((phi . n) (#) (ElementsOfPortfolioValueProb_fut (F,(G . n)))) . w
by VALUED_1:6;
hence
((phi . n) (#) (ElementsOfPortfolioValueProb_fut (F,(G . n)))) . w = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
by Def5000;
verum
end;
hence
RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
by A1, FUNCT_2:63; verum