let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being Real st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let F be SigmaField of Omega; :: thesis: for d being Nat st d > 0 holds
for r being Real st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let d be Nat; :: thesis: ( d > 0 implies for r being Real st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A1: d > 0 ; :: thesis: for r being Real st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let r be Real; :: thesis: ( r > - 1 implies for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A2: r > - 1 ; :: thesis: for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let phi be Real_Sequence; :: thesis: for jpi being pricefunction
for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let jpi be pricefunction ; :: thesis: for G being sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
set X = set_of_random_variables_on (F,Borel_Sets);
let G be sequence of (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 (d,phi,F,G,w) <= (PortfolioValueFut (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 (d,phi,F,G,w) <= (PortfolioValueFut (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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A4: BuyPortfolioExt (phi,jpi,d) <= 0 ; :: thesis: PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
A5: (1 + r) * (BuyPortfolioExt (phi,jpi,d)) <= 0

proof

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

end;

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