let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for jpi being pricefunction
for d, d2 being Nat st d > 0 & d2 = d - 1 holds
for Prob being Probability of F
for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
let F be SigmaField of Omega; :: thesis: for jpi being pricefunction
for d, d2 being Nat st d > 0 & d2 = d - 1 holds
for Prob being Probability of F
for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
let jpi be pricefunction ; :: thesis: for d, d2 being Nat st d > 0 & d2 = d - 1 holds
for Prob being Probability of F
for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
let d, d2 be Nat; :: thesis: ( d > 0 & d2 = d - 1 implies for Prob being Probability of F
for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) ) )
assume A1: ( d > 0 & d2 = d - 1 ) ; :: thesis: for Prob being Probability of F
for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
let Prob be Probability of F; :: thesis: for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
let r be Real; :: thesis: ( r > - 1 implies 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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) ) )
assume A2: r > - 1 ; :: 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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
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 ( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) ) )
assume A3: Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ; :: thesis: ( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
thus ( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d implies ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) ) :: thesis: ( ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) implies Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d )
proof
assume Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d ; :: thesis: ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 )
then consider phi being Real_Sequence such that
C1: ( BuyPortfolioExt (phi,jpi,d) <= 0 & Prob . (ArbitrageElSigma1 (phi,Omega,F,G,d)) = 1 & Prob . (ArbitrageElSigma2 (phi,Omega,F,G,d)) > 0 ) ;
ArbitrageElSigma1 (phi,Omega,F,G,d) = { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } by JB1;
then ArbitrageElSigma1 (phi,Omega,F,G,d) c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } by C1, A1, A2, A3, FINANCE1:14;
then C3: ArbitrageElSigma1 (phi,Omega,F,G,d) c= ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ by A1, JB2;
set RVspec = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[;
reconsider RVspec = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ as Event of F by JB3;
( 1 <= Prob . RVspec & Prob . RVspec <= 1 ) by PROB_1:35, C1, C3, PROB_1:34;
then Fin1: 1 = Prob . RVspec by XXREAL_0:1;
ArbitrageElSigma2 (phi,Omega,F,G,d) = { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } by JC1;
then ArbitrageElSigma2 (phi,Omega,F,G,d) c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } by C1, A1, A2, A3, FINANCE1:14;
then C3: ArbitrageElSigma2 (phi,Omega,F,G,d) c= ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ by A1, JC2;
set RVspec2 = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[;
reconsider RVspec2 = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ as Event of F by JC3;
Prob . (ArbitrageElSigma2 (phi,Omega,F,G,d)) <= Prob . RVspec2 by C3, PROB_1:34;
hence ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) by Fin1, C1; :: thesis: verum
end;
given myphi being Real_Sequence such that ASS0: ( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) ; :: thesis: Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d
deffunc H1( Nat) -> Element of REAL = In ((IFEQ ($1,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . $1))),REAL);
consider phi being Real_Sequence such that
AA1: for n being Element of NAT holds phi . n = H1(n) from FUNCT_2:sch 4();
 AA10: for n being Nat holds
( ( n = 0 implies phi . n = - (BuyPortfolio (myphi,jpi,d)) ) & ( n > 0 implies phi . n = myphi . n ) )
proof
let n be Nat; :: thesis: ( ( n = 0 implies phi . n = - (BuyPortfolio (myphi,jpi,d)) ) & ( n > 0 implies phi . n = myphi . n ) )
SS: n in NAT by ORDINAL1:def 12;
SU: myphi . n in REAL ;
SW: IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) in REAL
proof
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) in REAL
then IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) = - (BuyPortfolio (myphi,jpi,d)) by FUNCOP_1:def 8;
hence IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) in REAL by XREAL_0:def 1; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) in REAL
hence IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) in REAL by FUNCOP_1:def 8, SU; :: thesis: verum
end;
end;
end;
hereby :: thesis: ( n > 0 implies phi . n = myphi . n )
assume SQ: n = 0 ; :: thesis: phi . n = - (BuyPortfolio (myphi,jpi,d))
then phi . n = H1(n) by AA1
.= IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) by SUBSET_1:def 8, SW ;
hence phi . n = - (BuyPortfolio (myphi,jpi,d)) by FUNCOP_1:def 8, SQ; :: thesis: verum
end;
assume SQ: n > 0 ; :: thesis: phi . n = myphi . n
phi . n = In ((IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n))),REAL) by AA1, SS
.= IFEQ (n,0,(- (BuyPortfolio (myphi,jpi,d))),(myphi . n)) by SUBSET_1:def 8, SW ;
hence phi . n = myphi . n by FUNCOP_1:def 8, SQ; :: thesis: verum
end;
set B0 = - (BuyPortfolio (myphi,jpi,d));
Z1: BuyPortfolioExt (phi,jpi,d) = 0
proof
BuyPortfolioExt (phi,jpi,d) = (- (BuyPortfolio (myphi,jpi,d))) + (BuyPortfolio (myphi,jpi,d))
proof
zw: BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) by A1, FINANCE1:11;
(- (BuyPortfolio (phi,jpi,d))) + (BuyPortfolio (myphi,jpi,d)) = 0
proof
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) = (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . (d - 1)
proof
set P1 = Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1);
set P2 = Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1);
defpred S1[ Nat] means (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . $1 = (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . $1;
J0: S1[ 0 ]
proof
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0 = ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . 0 by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0 = (ElementsOfBuyPortfolio (phi,jpi)) . (0 + 1) by NAT_1:def 3;
then Erg1: (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0 = (phi . 1) * (jpi . 1) by VALUED_1:5;
(Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . 0 = ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1) . 0 by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . 0 = (ElementsOfBuyPortfolio (myphi,jpi)) . (0 + 1) by NAT_1:def 3;
then (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . 0 = (myphi . 1) * (jpi . 1) by VALUED_1:5;
hence S1[ 0 ] by Erg1, AA10; :: thesis: verum
end;
J1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume f1: S1[n] ; :: thesis: S1[n + 1]
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . n) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (n + 1)) by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . n) + ((ElementsOfBuyPortfolio (phi,jpi)) . ((n + 1) + 1)) by NAT_1:def 3;
then Erg1: (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . n) + ((phi . (n + 2)) * (jpi . (n + 2))) by VALUED_1:5;
set n2 = n + 2;
(Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . n) + (((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1) . (n + 1)) by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . n) + ((ElementsOfBuyPortfolio (myphi,jpi)) . ((n + 1) + 1)) by NAT_1:def 3;
then (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . n) + ((myphi . (n + 2)) * (jpi . (n + 2))) by VALUED_1:5;
hence S1[n + 1] by Erg1, f1, AA10; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(J0, J1);
 hence (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) = (Partial_Sums ((ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1)) . (d - 1) by A1; :: thesis: verum
end;
hence (- (BuyPortfolio (phi,jpi,d))) + (BuyPortfolio (myphi,jpi,d)) = 0 ; :: thesis: verum
end;
hence BuyPortfolioExt (phi,jpi,d) = (- (BuyPortfolio (myphi,jpi,d))) + (BuyPortfolio (myphi,jpi,d)) by zw, AA10; :: thesis: verum
end;
hence BuyPortfolioExt (phi,jpi,d) = 0 ; :: thesis: verum
end;
Z2: Prob . (ArbitrageElSigma1 (phi,Omega,F,G,d)) = 1
proof
set Set1 = RVPortfolioValueFutExt (phi,F,G,d);
set Set2 = (RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))));
(RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ = ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[
proof
for x being object holds
( x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ iff x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ )
proof
let x be object ; :: thesis: ( x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ iff x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ )
thus ( x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ implies x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ ) :: thesis: ( x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ implies x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ )
proof
assume sc: x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ ; :: thesis: x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[
then reconsider x = x as Element of Omega ;
(RVPortfolioValueFutExt (phi,F,G,d)) . x in [.0,+infty.[ by sc, FUNCT_1:def 7;
then PortfolioValueFutExt (d,phi,F,G,x) in [.0,+infty.[ by FINANCE3:def 1;
then e: ((1 + r) * (phi . 0)) + (PortfolioValueFut ((d2 + 1),phi,F,G,x)) in [.0,+infty.[ by A1, A3, FINANCE1:12;
( x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) & ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) . x in [.0,+infty.[ )
proof
- ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (- (BuyPortfolio (myphi,jpi,d))) ;
then uuu0: (1 + r) * (phi . 0) = - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) by AA10;
(RVPortfolioValueFut (myphi,F,G,d2)) . x = (RVPortfolioValueFut (phi,F,G,d2)) . x
proof
iii: (RVPortfolioValueFut (myphi,F,G,d2)) . x = PortfolioValueFut ((d2 + 1),myphi,F,G,x) by FINANCE3:def 3;
defpred S1[ Nat] means (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1 = (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1;
K1: S1[ 0 ]
proof
(Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . 0 by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . (0 + 1) by NAT_1:def 3;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (myphi . 1) by FINANCE1:def 10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (phi . 1) by AA10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . (0 + 1) by FINANCE1:def 10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . 0 by NAT_1:def 3;
hence S1[ 0 ] by SERIES_1:def 1; :: thesis: verum
end;
K2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AK2: S1[n] ; :: thesis: S1[n + 1]
set n1 = n + 1;
set n2 = (n + 1) + 1;
R: (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . n) + (((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1)) by AK2, SERIES_1:def 1;
((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . ((n + 1) + 1) by NAT_1:def 3;
then R1: ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . x) * (myphi . ((n + 1) + 1)) by FINANCE1:def 10;
((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1)
proof
((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . x) * (phi . ((n + 1) + 1)) by R1, AA10;
then ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . ((n + 1) + 1) by FINANCE1:def 10;
hence ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) by NAT_1:def 3; :: thesis: verum
end;
hence S1[n + 1] by SERIES_1:def 1, R; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(K1, K2);
 then (RVPortfolioValueFut (myphi,F,G,d2)) . x = PortfolioValueFut ((d2 + 1),phi,F,G,x) by iii;
hence (RVPortfolioValueFut (myphi,F,G,d2)) . x = (RVPortfolioValueFut (phi,F,G,d2)) . x by FINANCE3:def 3; :: thesis: verum
end;
then UUU: ((RVPortfolioValueFut (myphi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) in [.0,+infty.[ by uuu0, e, FINANCE3:def 3;
x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))))
proof
( dom (RVPortfolioValueFut (myphi,F,G,d2)) = Omega & dom (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) = Omega ) by FUNCT_2:def 1;
then (dom (RVPortfolioValueFut (myphi,F,G,d2))) /\ (dom (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))))) = Omega ;
then dom ((RVPortfolioValueFut (myphi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))))) = Omega by VALUED_1:def 1;
hence x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))))) ; :: thesis: verum
end;
hence ( x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) & ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) . x in [.0,+infty.[ ) by UUU, VALUED_1:13; :: thesis: verum
end;
hence x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ by FUNCT_1:def 7; :: thesis: verum
end;
assume ab: x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ ; :: thesis: x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[
then ABC1: ( x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) & ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) . x in [.0,+infty.[ ) by FUNCT_1:def 7;
reconsider x = x as Element of Omega by ab;
ABC3: ((RVPortfolioValueFut (myphi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) in [.0,+infty.[ by ABC1, VALUED_1:13;
- ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (phi . 0)
proof
- ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (- (BuyPortfolio (myphi,jpi,d))) ;
hence - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (phi . 0) by AA10; :: thesis: verum
end;
then ABC4: (PortfolioValueFut ((d2 + 1),myphi,F,G,x)) + ((1 + r) * (phi . 0)) in [.0,+infty.[ by FINANCE3:def 3, ABC3;
ABC2: (RVPortfolioValueFutExt (phi,F,G,d)) . x in [.0,+infty.[
proof
PortfolioValueFut ((d2 + 1),phi,F,G,x) = PortfolioValueFut ((d2 + 1),myphi,F,G,x)
proof
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . d2 = (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . d2
proof
defpred S1[ Nat] means (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1 = (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1;
K1: S1[ 0 ]
proof
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . 0 by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . (0 + 1) by NAT_1:def 3;
then R: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (phi . 1) by FINANCE1:def 10;
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (myphi . 1) by R, AA10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . (0 + 1) by FINANCE1:def 10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . 0 by NAT_1:def 3;
hence S1[ 0 ] by SERIES_1:def 1; :: thesis: verum
end;
K2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
set n2 = (n + 1) + 1;
assume S1[n] ; :: thesis: S1[n + 1]
then R: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . n) + (((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1)) by SERIES_1:def 1;
((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1)
proof
((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . ((n + 1) + 1) by NAT_1:def 3;
then QA: ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . x) * (phi . ((n + 1) + 1)) by FINANCE1:def 10;
phi . ((n + 1) + 1) = myphi . ((n + 1) + 1) by AA10;
then ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . ((n + 1) + 1) by FINANCE1:def 10, QA;
hence ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) by NAT_1:def 3; :: thesis: verum
end;
hence S1[n + 1] by SERIES_1:def 1, R; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(K1, K2);
 hence (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . d2 = (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . d2 ; :: thesis: verum
end;
hence PortfolioValueFut ((d2 + 1),phi,F,G,x) = PortfolioValueFut ((d2 + 1),myphi,F,G,x) ; :: thesis: verum
end;
then PortfolioValueFutExt ((d2 + 1),phi,F,G,x) in [.0,+infty.[ by A3, FINANCE1:12, ABC4;
hence (RVPortfolioValueFutExt (phi,F,G,d)) . x in [.0,+infty.[ by A1, FINANCE3:def 1; :: thesis: verum
end;
dom (RVPortfolioValueFutExt (phi,F,G,d)) = Omega by FUNCT_2:def 1;
hence x in (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ by FUNCT_1:def 7, ABC2; :: thesis: verum
end;
hence (RVPortfolioValueFutExt (phi,F,G,d)) " [.0,+infty.[ = ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[ by TARSKI:2; :: thesis: verum
end;
hence Prob . (ArbitrageElSigma1 (phi,Omega,F,G,d)) = 1 by ASS0; :: thesis: verum
end;
Prob . (ArbitrageElSigma2 (phi,Omega,F,G,d)) > 0
proof
(RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ = ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[
proof
set Set1 = RVPortfolioValueFutExt (phi,F,G,d);
set Set2 = (RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))));
for x being object holds
( x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ iff x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ )
proof
let x be object ; :: thesis: ( x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ iff x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ )
thus ( x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ implies x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ ) :: thesis: ( x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ implies x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ )
proof
assume ss: x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ ; :: thesis: x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[
then s: ( x in dom (RVPortfolioValueFutExt (phi,F,G,d)) & (RVPortfolioValueFutExt (phi,F,G,d)) . x in ].0,+infty.[ ) by FUNCT_1:def 7;
reconsider x = x as Element of Omega by ss;
PortfolioValueFutExt (d,phi,F,G,x) in ].0,+infty.[ by FINANCE3:def 1, s;
then e: ((1 + r) * (phi . 0)) + (PortfolioValueFut ((d2 + 1),phi,F,G,x)) in ].0,+infty.[ by A1, A3, FINANCE1:12;
- ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (- (BuyPortfolio (myphi,jpi,d))) ;
then uuu0: (1 + r) * (phi . 0) = - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) by AA10;
iii: (RVPortfolioValueFut (myphi,F,G,d2)) . x = PortfolioValueFut ((d2 + 1),myphi,F,G,x) by FINANCE3:def 3;
( x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) & ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) . x in ].0,+infty.[ )
proof
(RVPortfolioValueFut (myphi,F,G,d2)) . x = (RVPortfolioValueFut (phi,F,G,d2)) . x
proof
defpred S1[ Nat] means (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1 = (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1;
K1: S1[ 0 ]
proof
(Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . 0 by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . (0 + 1) by NAT_1:def 3;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (myphi . 1) by FINANCE1:def 10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (phi . 1) by AA10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . (0 + 1) by FINANCE1:def 10;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . 0 by NAT_1:def 3;
hence S1[ 0 ] by SERIES_1:def 1; :: thesis: verum
end;
K2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume AK2: S1[n] ; :: thesis: S1[n + 1]
set n1 = n + 1;
set n2 = (n + 1) + 1;
R: (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . n) + (((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1)) by AK2, SERIES_1:def 1;
((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1)
proof
((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . ((n + 1) + 1) by NAT_1:def 3;
then R1: ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . x) * (myphi . ((n + 1) + 1)) by FINANCE1:def 10;
((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . x) * (phi . ((n + 1) + 1)) by R1, AA10;
then ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . ((n + 1) + 1) by FINANCE1:def 10;
hence ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) by NAT_1:def 3; :: thesis: verum
end;
hence S1[n + 1] by SERIES_1:def 1, R; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(K1, K2);
 then (RVPortfolioValueFut (myphi,F,G,d2)) . x = PortfolioValueFut ((d2 + 1),phi,F,G,x) by iii;
hence (RVPortfolioValueFut (myphi,F,G,d2)) . x = (RVPortfolioValueFut (phi,F,G,d2)) . x by FINANCE3:def 3; :: thesis: verum
end;
then UUU: ((RVPortfolioValueFut (myphi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) in ].0,+infty.[ by uuu0, e, FINANCE3:def 3;
x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))))
proof
( dom (RVPortfolioValueFut (myphi,F,G,d2)) = Omega & dom (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) = Omega ) by FUNCT_2:def 1;
then (dom (RVPortfolioValueFut (myphi,F,G,d2))) /\ (dom (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))))) = Omega ;
then dom ((RVPortfolioValueFut (myphi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))))) = Omega by VALUED_1:def 1;
hence x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) + (- (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))))) ; :: thesis: verum
end;
hence ( x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) & ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) . x in ].0,+infty.[ ) by UUU, VALUED_1:13; :: thesis: verum
end;
hence x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ by FUNCT_1:def 7; :: thesis: verum
end;
assume ab: x in ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ ; :: thesis: x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[
then ABC1: ( x in dom ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) & ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) . x in ].0,+infty.[ ) by FUNCT_1:def 7;
reconsider x = x as Element of Omega by ab;
ABC3: ((RVPortfolioValueFut (myphi,F,G,d2)) . x) - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) in ].0,+infty.[ by ABC1, VALUED_1:13;
- ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (- (BuyPortfolio (myphi,jpi,d))) ;
then - ((Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d)))) . x) = (1 + r) * (phi . 0) by AA10;
then ABC4: (PortfolioValueFut ((d2 + 1),myphi,F,G,x)) + ((1 + r) * (phi . 0)) in ].0,+infty.[ by FINANCE3:def 3, ABC3;
ABC2: (RVPortfolioValueFutExt (phi,F,G,d)) . x in ].0,+infty.[
proof
PortfolioValueFut ((d2 + 1),phi,F,G,x) = PortfolioValueFut ((d2 + 1),myphi,F,G,x)
proof
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . d2 = (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . d2
proof
defpred S1[ Nat] means (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1 = (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1;
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . 0 by SERIES_1:def 1;
then (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . (0 + 1) by NAT_1:def 3;
then R: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . 0 = ((ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (phi . 1) by FINANCE1:def 10;
K1: S1[ 0 ] K2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set n1 = n + 1;
set n2 = (n + 1) + 1;
assume S1[n] ; :: thesis: S1[n + 1]
then R: (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . (n + 1) = ((Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . n) + (((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1)) by SERIES_1:def 1;
((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1)
proof
((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (phi,F,x,G)) . ((n + 1) + 1) by NAT_1:def 3;
then QA: ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValueProb_fut (F,(G . ((n + 1) + 1)))) . x) * (phi . ((n + 1) + 1)) by FINANCE1:def 10;
phi . ((n + 1) + 1) = myphi . ((n + 1) + 1) by AA10;
then ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = (ElementsOfPortfolioValue_fut (myphi,F,x,G)) . ((n + 1) + 1) by FINANCE1:def 10, QA;
hence ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . (n + 1) = ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . (n + 1) by NAT_1:def 3; :: thesis: verum
end;
hence S1[n + 1] by SERIES_1:def 1, R; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(K1, K2);
 hence (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . d2 = (Partial_Sums ((ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . d2 ; :: thesis: verum
end;
hence PortfolioValueFut ((d2 + 1),phi,F,G,x) = PortfolioValueFut ((d2 + 1),myphi,F,G,x) ; :: thesis: verum
end;
then PortfolioValueFutExt ((d2 + 1),phi,F,G,x) in ].0,+infty.[ by A3, FINANCE1:12, ABC4;
hence (RVPortfolioValueFutExt (phi,F,G,d)) . x in ].0,+infty.[ by A1, FINANCE3:def 1; :: thesis: verum
end;
dom (RVPortfolioValueFutExt (phi,F,G,d)) = Omega by FUNCT_2:def 1;
hence x in (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ by FUNCT_1:def 7, ABC2; :: thesis: verum
end;
hence (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[ = ((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[ by TARSKI:2; :: thesis: verum
end;
hence Prob . (ArbitrageElSigma2 (phi,Omega,F,G,d)) > 0 by ASS0; :: thesis: verum
end;
hence Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d by Z1, Z2; :: thesis: verum