let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for d being natural number st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let F be SigmaField of Omega; :: thesis: for d being natural number st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let d be natural number ; :: thesis: ( d > 0 implies for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A0: d > 0 ; :: thesis: for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let r be real number ; :: thesis: ( r > - 1 implies for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A1: r > - 1 ; :: thesis: for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let phi be Real_Sequence; :: thesis: for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let jpi be pricefunction ; :: thesis: for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
set X = set_of_random_variables_on (F,Borel_Sets);
let G be Function of NAT,(set_of_random_variables_on (F,Borel_Sets)); :: thesis: ( Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 implies ( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A3: Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ; :: thesis: ( not BuyPortfolioExt (phi,jpi,d) <= 0 or ( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume J0: BuyPortfolioExt (phi,jpi,d) <= 0 ; :: thesis: ( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
J3: { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } or x in { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
assume x in { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } ; :: thesis: x in { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }
then consider w being Element of Omega such that
AJ0: ( x = w & PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 ) ;
0 <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A0, A1, A3, J0, Th8, AJ0;
then 0 + ((1 + r) * (BuyPortfolio (phi,jpi,d))) <= PortfolioValueFut (r,d,phi,F,G,w) by XREAL_1:19;
hence x in { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } by AJ0; :: thesis: verum

end;

{ w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } or x in { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
assume x in { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } ; :: thesis: x in { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) }
then consider w being Element of Omega such that
AJ0: ( x = w & PortfolioValueFutExt (r,d,phi,F,G,w) > 0 ) ;
PortfolioValueFutExt (r,d,phi,F,G,w) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A0, A1, A3, J0, Th8;
then 0 + ((1 + r) * (BuyPortfolio (phi,jpi,d))) < ((PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))) + ((1 + r) * (BuyPortfolio (phi,jpi,d))) by AJ0, XREAL_1:6;
hence x in { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } by AJ0; :: thesis: verum

end;

hence ( { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) by J3; :: thesis: verum