RVPortfolioValueFutExt (phi,F,G,n) is F, Borel_Sets -random_variable-like by FINANCE3:6;
hence (RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ is Element of F by A1; :: thesis: verum