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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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) implies for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (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: for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (r,d,phi,F,G,w) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let w be Element of Omega; :: thesis: ( BuyPortfolioExt (phi,jpi,d) <= 0 implies PortfolioValueFutExt (r,d,phi,F,G,w) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A4: BuyPortfolioExt (phi,jpi,d) <= 0 ; :: thesis: PortfolioValueFutExt (r,d,phi,F,G,w) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
A5: (1 + r) * (BuyPortfolioExt (phi,jpi,d)) <= 0

proof

1 + r > 0 by A1, XREAL_1:62;
hence (1 + r) * (BuyPortfolioExt (phi,jpi,d)) <= 0 by A4; :: thesis: verum

end;

((1 + r) * (BuyPortfolioExt (phi,jpi,d))) + ((PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolioExt (phi,jpi,d)))) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolioExt (phi,jpi,d))) by A5, XREAL_1:32;
then PortfolioValueFut (r,d,phi,F,G,w) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * ((phi . 0) + (BuyPortfolio (phi,jpi,d)))) by A0, Th6;
then PortfolioValueFut (r,d,phi,F,G,w) <= ((PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))) - ((1 + r) * (phi . 0)) ;
then (PortfolioValueFut (r,d,phi,F,G,w)) + ((1 + r) * (phi . 0)) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by XREAL_1:19;
hence PortfolioValueFutExt (r,d,phi,F,G,w) <= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A0, A3, Th7; :: thesis: verum