set RV = RVPortfolioValueFutExt (phi,F,G,n);
RVPortfolioValueFutExt (phi,F,G,n) is random_variable of F, Borel_Sets by FINANCE3:6;
then RVPortfolioValueFutExt (phi,F,G,n) is_random_variable_on F, Borel_Sets by RANDOM_3:def 1;
hence (RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ is Element of F by A1; :: thesis: verum