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