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

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

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) * (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;
1 + r > 0
by A2, XREAL_1:62;

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

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

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