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 n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) 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 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)); :: thesis: 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; :: thesis: for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
let n be Nat; :: thesis: 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; :: thesis: ((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; :: thesis: verum

end;

hence RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets by A1, FUNCT_2:63; :: thesis: verum