let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ in F
let F be SigmaField of Omega; :: thesis: for phi being Real_Sequence
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ in F
let phi be Real_Sequence; :: thesis: for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ in F
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); :: thesis: for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ in F
let n be Nat; :: thesis: (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ in F
set RV = RVPortfolioValueFutExt (phi,F,G,n);
A1: [.0,+infty.[ is Element of Borel_Sets by FINANCE1:3;
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.[ in F by A1; :: thesis: verum