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
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;
reconsider constRV = Omega --> myr as random_variable of F, Borel_Sets by FINANCE3:10;
B5: [.0,+infty.[ is Element of Borel_Sets by FINANCE1:3;
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 B5; :: thesis: verum