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 st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
let F be SigmaField of Omega; :: thesis: for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
let phi be Real_Sequence; :: thesis: for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
let jpi be pricefunction ; :: thesis: for d, d2 being Nat st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
let d, d2 be Nat; :: thesis: ( d2 = d - 1 implies for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ )
assume a10: d2 = d - 1 ; :: thesis: for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
let r be Real; :: thesis: for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); :: thesis: { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
set Set1 = { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ;
set Set2 = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[;
for x being object holds
( x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } iff x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ )

proof

let x be object ; :: thesis: ( x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } iff x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ )
thus ( x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } implies x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ ) :: thesis: ( x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ implies x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )

proof

assume x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ; :: thesis: x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
then consider w being Element of Omega such that
A1: ( w = x & PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) ) ;
reconsider x = x as Element of Omega by A1;
set myel = (1 + r) * (BuyPortfolio (phi,jpi,d));
a2: PortfolioValueFut ((d2 + 1),phi,F,G,w) = (RVPortfolioValueFut (phi,F,G,d2)) . w by FINANCE3:def 3;
((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x) > 0 by XREAL_1:50, A1, a2, a10;
then Q1: ((RVPortfolioValueFut (phi,F,G,d2)) . x) + ((- 1) * ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x)) > 0 ;
x in dom (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) ;
then x in dom ((- 1) (#) (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) by VALUED_1:def 5;
then ((RVPortfolioValueFut (phi,F,G,d2)) . x) + (((- 1) (#) (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x) > 0 by Q1, VALUED_1:def 5;
then ( 0 < ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x & ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x < +infty ) by XXREAL_0:9, VALUED_1:1;
then T1: ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x in ].0,+infty.[ by XXREAL_1:4;
dom ((RVPortfolioValueFut (phi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))))) = Omega /\ Omega by FUNCT_2:def 1;
hence x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ by T1, FUNCT_1:def 7; :: thesis: verum

end;

assume a1: x in ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ ; :: thesis: x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) }
then A1: ( x in dom ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) & ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x in ].0,+infty.[ ) by FUNCT_1:def 7;
set my1 = (1 + r) * (BuyPortfolio (phi,jpi,d));
set my2 = (RVPortfolioValueFut (phi,F,G,d2)) . x;
reconsider x = x as Element of Omega by a1;
set RVmyx = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x;
((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x = ((RVPortfolioValueFut (phi,F,G,d2)) . x) + (((- 1) (#) (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x) by VALUED_1:1;
then ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) . x = ((RVPortfolioValueFut (phi,F,G,d2)) . x) + ((- 1) * ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x)) by VALUED_1:6;
then 0 < ((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d)))) . x) by A1, XXREAL_1:4;
then 0 < ((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) ;
then 0 + ((1 + r) * (BuyPortfolio (phi,jpi,d))) < (((RVPortfolioValueFut (phi,F,G,d2)) . x) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))) + ((1 + r) * (BuyPortfolio (phi,jpi,d))) by XREAL_1:6;
then (1 + r) * (BuyPortfolio (phi,jpi,d)) < PortfolioValueFut ((d2 + 1),phi,F,G,x) by FINANCE3:def 3;
hence x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } by a10; :: thesis: verum

end;

hence { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ by TARSKI:2; :: thesis: verum