set RV = RVPortfolioValueFutExt (phi,F,G,n);
A1:
[.0,+infty.[ is Element of Borel_Sets
by FINANCE1:3;
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; verum