let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
let F be SigmaField of Omega; :: thesis: for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
let phi be Real_Sequence; :: thesis: for jpi being pricefunction
for d, d2 being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
let jpi be pricefunction ; :: thesis: for d, d2 being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
let d, d2 be Nat; :: thesis: for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
let r be Real; :: thesis: for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); :: thesis: ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
( {0} is Element of Borel_Sets & [.0,+infty.[ is Element of Borel_Sets ) by FINANCE1:3, FINANCE2:5;
then B1: ].0,+infty.[ is Element of Borel_Sets by PROB_1:6, ZZ;
set RV = RVPortfolioValueFut (phi,F,G,d2);
reconsider RV = RVPortfolioValueFut (phi,F,G,d2) as random_variable of F, Borel_Sets by FINANCE3:7;
set myr = (1 + r) * (BuyPortfolio (phi,jpi,d));
reconsider myr = (1 + r) * (BuyPortfolio (phi,jpi,d)) as Element of REAL by XREAL_0:def 1;
set constRV = Omega --> myr;
reconsider constRV = Omega --> myr as random_variable of F, Borel_Sets by FINANCE3:10;
RV - constRV is F, Borel_Sets -random_variable-like by FINANCE2:24;
hence ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F by B1; :: thesis: verum