let Prob be Probability of Special_SigmaField1 ; :: thesis: for G being sequence of (set_of_random_variables_on (Special_SigmaField1,Borel_Sets)) st G . 0 = {1,2,3,4} --> 1 & G . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
G . k = {1,2,3,4} --> 0 ) holds
ex jpi being pricefunction st Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1
set Omega = {1,2,3,4};
set F = Special_SigmaField1 ;
let G be sequence of (set_of_random_variables_on (Special_SigmaField1,Borel_Sets)); :: thesis: ( G . 0 = {1,2,3,4} --> 1 & G . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
G . k = {1,2,3,4} --> 0 ) implies ex jpi being pricefunction st Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1 )
assume A3: ( G . 0 = {1,2,3,4} --> 1 & G . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
G . k = {1,2,3,4} --> 0 ) ) ; :: thesis: ex jpi being pricefunction st Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1
ZW: ( Prob . {1,2,3,4} = 1 & Prob . {} = 0 )
proof
Prob . {1,2,3,4} = Prob . ([#] Special_SigmaField1) ;
then B2: Prob . {1,2,3,4} = 1 by PROB_1:30;
reconsider A = {} as Event of Special_SigmaField1 by PROB_1:4;
Prob . (([#] Special_SigmaField1) \ A) = Prob . ([#] Special_SigmaField1) ;
then (Prob . ([#] Special_SigmaField1)) + (Prob . A) = 1 by PROB_1:31;
hence ( Prob . {1,2,3,4} = 1 & Prob . {} = 0 ) by B2; :: thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of REAL = In ((IFEQ ($1,0,1,(IFEQ ($1,1,1,0)))),REAL);
consider f being Function of NAT,REAL such that
C1: for d being Element of NAT holds f . d = H1(d) from FUNCT_2:sch 4();
 f is pricefunction
proof
d0: f . 0 = H1( 0 ) by C1;
for n being Element of NAT holds f . n >= 0
proof
let n be Element of NAT ; :: thesis: f . n >= 0
f . n = H1(n) by C1;
hence f . n >= 0 ; :: thesis: verum
end;
hence f is pricefunction by d0, FINANCE1:def 2, FUNCOP_1:def 8; :: thesis: verum
end;
then reconsider jpi = f as pricefunction ;
deffunc H2( Element of NAT ) -> Element of REAL = In ((IFEQ ($1,0,(- 1),(IFEQ ($1,1,1,0)))),REAL);
a0: H2( 0 ) = In ((- 1),REAL) by FUNCOP_1:def 8
.= - 1 ;
a1: H2(1) = In ((IFEQ (1,1,1,0)),REAL) by FUNCOP_1:def 8
.= 1 by FUNCOP_1:def 8 ;
consider phi being Real_Sequence such that
A4: for k being Element of NAT holds phi . k = H2(k) from FUNCT_2:sch 4();
 FinJ: ( Prob . (ArbitrageElSigma1 (phi,{1,2,3,4},Special_SigmaField1,G,1)) = 1 & Prob . (ArbitrageElSigma2 (phi,{1,2,3,4},Special_SigmaField1,G,1)) > 0 & BuyPortfolioExt (phi,jpi,1) <= 0 )
proof
G1: BuyPortfolioExt (phi,jpi,1) <= 0
proof
(Partial_Sums (phi (#) jpi)) . 1 = ((Partial_Sums (phi (#) jpi)) . 0) + ((phi (#) jpi) . (0 + 1)) by SERIES_1:def 1;
then H1: (Partial_Sums (phi (#) jpi)) . 1 = ((phi (#) jpi) . 0) + ((phi (#) jpi) . 1) by SERIES_1:def 1;
H2: (phi (#) jpi) . 0 = - 1
proof
aa: IFEQ (0,0,(- 1),(IFEQ (0,1,1,0))) = - 1 by FUNCOP_1:def 8;
(phi (#) jpi) . 0 = (phi . 0) * (jpi . 0) by VALUED_1:5;
then (phi (#) jpi) . 0 = H2( 0 ) * (f . 0) by A4;
then (phi (#) jpi) . 0 = (- 1) * (In ((IFEQ (0,0,1,(IFEQ (0,1,1,0)))),REAL)) by C1, aa;
then (phi (#) jpi) . 0 = (- 1) * 1 by FUNCOP_1:def 8;
hence (phi (#) jpi) . 0 = - 1 ; :: thesis: verum
end;
(phi (#) jpi) . 1 = 1
proof
aa: IFEQ (1,0,(- 1),(IFEQ (1,1,1,0))) = IFEQ (1,1,1,0) by FUNCOP_1:def 8;
(phi (#) jpi) . 1 = (phi . 1) * (jpi . 1) by VALUED_1:5;
then (phi (#) jpi) . 1 = H2(1) * (f . 1) by A4
.= 1 * (f . 1) by aa, FUNCOP_1:def 8
.= 1 * (In ((IFEQ (1,0,1,(IFEQ (1,1,1,0)))),REAL)) by C1
.= 1 * (IFEQ (1,1,1,0)) by FUNCOP_1:def 8 ;
hence (phi (#) jpi) . 1 = 1 by FUNCOP_1:def 8; :: thesis: verum
end;
hence BuyPortfolioExt (phi,jpi,1) <= 0 by H2, H1; :: thesis: verum
end;
set RV = RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1);
( Prob . (ArbitrageElSigma1 (phi,{1,2,3,4},Special_SigmaField1,G,1)) = 1 & Prob . (ArbitrageElSigma2 (phi,{1,2,3,4},Special_SigmaField1,G,1)) > 0 )
proof
fin1: {1,2,3,4} = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[
proof
for x being object holds
( x in {1,2,3,4} iff x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ )
proof
let x be object ; :: thesis: ( x in {1,2,3,4} iff x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ )
( x in {1,2,3,4} implies x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ )
proof
assume x in {1,2,3,4} ; :: thesis: x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[
then reconsider x = x as Element of {1,2,3,4} ;
q1: dom (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) = {1,2,3,4} by FUNCT_2:def 1;
( x in dom (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x in [.0,+infty.[ )
proof
set RVh1 = RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0);
(RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,(0 + 1))) . x ;
then (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x = ((RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) + (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0))) . x by FINANCE3:9;
then S0: (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x = ((RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x) + ((RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x) by VALUED_1:1;
( 0 <= (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x < +infty )
proof
S1: (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = - 1
proof
(RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValueProb_fut (Special_SigmaField1,(G . 0))) . x) * (phi . 0) by FINANCE2:def 5;
then K1: (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = ((Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 0))) . x) * (phi . 0) by FINANCE1:def 8;
set G0 = G . 0;
K2: G . 0 = Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 0)) by FINANCE1:def 7;
reconsider G0 = G . 0 as Function of {1,2,3,4},REAL by K1, FINANCE1:def 7;
(RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = 1 * (phi . 0) by A3, K1, K2;
then (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = 1 * H2( 0 ) by A4
.= In ((- 1),REAL) by FUNCOP_1:def 8 ;
hence (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = - 1 ; :: thesis: verum
end;
set RV0 = RVPortfolioValueFut (phi,Special_SigmaField1,G,0);
(RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = 5
proof
(RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = PortfolioValueFut ((0 + 1),phi,Special_SigmaField1,G,x) by FINANCE3:def 3;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValue_fut (phi,Special_SigmaField1,x,G)) ^\ 1) . 0 by SERIES_1:def 1;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = (ElementsOfPortfolioValue_fut (phi,Special_SigmaField1,x,G)) . (0 + 1) by NAT_1:def 3;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValueProb_fut (Special_SigmaField1,(G . 1))) . x) * (phi . 1) by FINANCE1:def 10;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValueProb_fut (Special_SigmaField1,(G . 1))) . x) * H2(1) by A4;
then R1: (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 1))) . x) * 1 by a1, FINANCE1:def 8;
G . 1 = Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 1)) by FINANCE1:def 7;
then reconsider G1 = G . 1 as Function of {1,2,3,4},REAL ;
(RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = (G1 . x) * 1 by R1, FINANCE1:def 7;
hence (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = 5 by A3; :: thesis: verum
end;
hence ( 0 <= (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x < +infty ) by XXREAL_0:9, S0, S1; :: thesis: verum
end;
hence ( x in dom (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x in [.0,+infty.[ ) by q1, XXREAL_1:3; :: thesis: verum
end;
hence x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ by FUNCT_1:def 7; :: thesis: verum
end;
hence ( x in {1,2,3,4} iff x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ ) ; :: thesis: verum
end;
hence {1,2,3,4} = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ by TARSKI:2; :: thesis: verum
end;
{1,2,3,4} = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[
proof
for x being object holds
( x in {1,2,3,4} iff x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ )
proof
let x be object ; :: thesis: ( x in {1,2,3,4} iff x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ )
thus ( x in {1,2,3,4} implies x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ ) :: thesis: ( x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ implies x in {1,2,3,4} )
proof
assume x in {1,2,3,4} ; :: thesis: x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[
then reconsider x = x as Element of {1,2,3,4} ;
q1: dom (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) = {1,2,3,4} by FUNCT_2:def 1;
( x in dom (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x in ].0,+infty.[ )
proof
set RVh1 = RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0);
(RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,(0 + 1))) . x ;
then (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x = ((RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) + (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0))) . x by FINANCE3:9;
then S0: (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x = ((RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x) + ((RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x) by VALUED_1:1;
( 0 < (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x < +infty )
proof
(RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValueProb_fut (Special_SigmaField1,(G . 0))) . x) * (phi . 0) by FINANCE2:def 5;
then K1: (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = ((Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 0))) . x) * (phi . 0) by FINANCE1:def 8;
set G0 = G . 0;
K2: G . 0 = Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 0)) by FINANCE1:def 7;
reconsider G0 = G . 0 as Function of {1,2,3,4},REAL by K1, FINANCE1:def 7;
(RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = 1 * (phi . 0) by A3, K1, K2;
then S1: (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = - 1 by a0, A4;
set RV0 = RVPortfolioValueFut (phi,Special_SigmaField1,G,0);
(RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = PortfolioValueFut ((0 + 1),phi,Special_SigmaField1,G,x) by FINANCE3:def 3;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValue_fut (phi,Special_SigmaField1,x,G)) ^\ 1) . 0 by SERIES_1:def 1;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = (ElementsOfPortfolioValue_fut (phi,Special_SigmaField1,x,G)) . (0 + 1) by NAT_1:def 3;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValueProb_fut (Special_SigmaField1,(G . 1))) . x) * (phi . 1) by FINANCE1:def 10;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((ElementsOfPortfolioValueProb_fut (Special_SigmaField1,(G . 1))) . x) * H2(1) by A4;
then R1: (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = ((Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 1))) . x) * 1 by a1, FINANCE1:def 8;
G . 1 = Change_Element_to_Func (Special_SigmaField1,Borel_Sets,(G . 1)) by FINANCE1:def 7;
then reconsider G1 = G . 1 as Function of {1,2,3,4},REAL ;
(RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = (G1 . x) * 1 by R1, FINANCE1:def 7;
then (RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = 5 by A3;
hence ( 0 < (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x < +infty ) by XXREAL_0:9, S0, S1; :: thesis: verum
end;
hence ( x in dom (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x in ].0,+infty.[ ) by q1, XXREAL_1:4; :: thesis: verum
end;
hence x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ by FUNCT_1:def 7; :: thesis: verum
end;
thus ( x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ implies x in {1,2,3,4} ) ; :: thesis: verum
end;
hence {1,2,3,4} = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ by TARSKI:2; :: thesis: verum
end;
hence ( Prob . (ArbitrageElSigma1 (phi,{1,2,3,4},Special_SigmaField1,G,1)) = 1 & Prob . (ArbitrageElSigma2 (phi,{1,2,3,4},Special_SigmaField1,G,1)) > 0 ) by fin1, ZW; :: thesis: verum
end;
hence ( Prob . (ArbitrageElSigma1 (phi,{1,2,3,4},Special_SigmaField1,G,1)) = 1 & Prob . (ArbitrageElSigma2 (phi,{1,2,3,4},Special_SigmaField1,G,1)) > 0 & BuyPortfolioExt (phi,jpi,1) <= 0 ) by G1; :: thesis: verum
end;
take jpi ; :: thesis: Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1
thus Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1 by FinJ; :: thesis: verum