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 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 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 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 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 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 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 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 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 ; :: 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 ;
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 ;
then PortfolioValueFut (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ((phi . 0) + (BuyPortfolio (phi,jpi,d)))) by ;
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