let Prob be Probability of Special_SigmaField1 ; :: thesis:
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:
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:
ZW: ( Prob . {1,2,3,4} = 1 & Prob . {} = 0 )

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:

end;

deffunc H₁( Nat) -> Element of REAL = Conv2 ($1,1);
consider f being Real_Sequence such that
C1: for d being Element of NAT holds f . d = H₁(d) from FUNCT_2:sch 4();
f is pricefunction

proof

d0: f . 0 = Conv2 (0,1) by C1;
for n being Element of NAT holds f . n >= 0

proof

let n be Element of NAT ; :: thesis:
d1: f . n = Conv2 (n,1) by C1;

per cases ;

suppose n = 0 ; :: thesis:

hence f . n >= 0 by d1, Def3; :: thesis:

end;

suppose n > 0 ; :: thesis:

then f . n = Conv (n,1) by d1, Def3;
hence f . n >= 0 by Def2; :: thesis:

end;

hence f is pricefunction by d0, Def3, FINANCE1:def 2; :: thesis:

end;

then consider jpi being pricefunction such that
A30: jpi = f ;
deffunc H₂( Nat) -> Element of REAL = Conv4 ($1,1);
consider phi being Real_Sequence such that
A4: for k being Element of NAT holds phi . k = H₂(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

(phi (#) jpi) . 0 = (phi . 0) * (jpi . 0) by VALUED_1:5;
then (phi (#) jpi) . 0 = (Conv4 (0,1)) * (f . 0) by A4, A30;
then (phi (#) jpi) . 0 = (- 1) * (f . 0) by Def5;
then (phi (#) jpi) . 0 = (- 1) * (Conv2 (0,1)) by C1;
then (phi (#) jpi) . 0 = (- 1) * 1 by Def3;
hence (phi (#) jpi) . 0 = - 1 ; :: thesis:

end;

(phi (#) jpi) . 1 = 1

proof

(phi (#) jpi) . 1 = (phi . 1) * (jpi . 1) by VALUED_1:5;
then (phi (#) jpi) . 1 = (Conv4 (1,1)) * (f . 1) by A4, A30
.= (Conv (1,1)) * (f . 1) by Def5
.= 1 * (f . 1) by Def2
.= 1 * (Conv2 (1,1)) by C1
.= 1 * (Conv (1,1)) by Def3 ;
hence (phi (#) jpi) . 1 = 1 by Def2; :: thesis:

end;

hence BuyPortfolioExt (phi,jpi,1) <= 0 by H2, H1; :: thesis:

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} implies x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ )

proof

assume x in {1,2,3,4} ; :: thesis:
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

S1: (RVElementsOfPortfolioValue_fut (phi,Special_SigmaField1,G,0)) . x = - 1

proof

end;

set RV0 = RVPortfolioValueFut (phi,Special_SigmaField1,G,0);
(RVPortfolioValueFut (phi,Special_SigmaField1,G,0)) . x = 5

proof

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:

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:

end;

hence x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ by FUNCT_1:def 7; :: thesis:

end;

hence ( x in {1,2,3,4} iff x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ ) ; :: thesis:

end;

hence {1,2,3,4} = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " [.0,+infty.[ by TARSKI:2; :: thesis:

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:
thus ( x in {1,2,3,4} implies x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ ) :: thesis:

proof

( 0 < (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x & (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) . x < +infty )

proof

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:

end;

hence x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ by FUNCT_1:def 7; :: thesis:

end;

thus ( x in (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ implies x in {1,2,3,4} ) ; :: thesis:

end;

hence {1,2,3,4} = (RVPortfolioValueFutExt (phi,Special_SigmaField1,G,1)) " ].0,+infty.[ by TARSKI:2; :: thesis:

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:

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:

end;

take jpi ; :: thesis:
thus Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1 by FinJ; :: thesis: