finance6.miz



    begin

    reserve Omega for non empty set;

    reserve F for SigmaField of Omega;

    theorem :: FINANCE6:1

    

     A1: ]. 0 , +infty .[ is Element of Borel_Sets

    proof

      set Bor1 = ]. 0 , +infty .[;

      reconsider Bor3 = { 0 } as Event of Borel_Sets by FINANCE2: 5;

      reconsider Bor2 = [. 0 , +infty .[ as Event of Borel_Sets by FINANCE1: 3;

      Bor1 = (Bor2 \ Bor3)

      proof

        for x be object holds x in Bor1 iff (x in (Bor2 \ Bor3))

        proof

          let x be object;

          thus x in Bor1 implies x in (Bor2 \ Bor3)

          proof

            assume

             ASS0: x in Bor1;

            then

            reconsider x as Real;

            

             d1: 0 < x & x < +infty by ASS0, XXREAL_1: 4;

            then

             D2: x in [. 0 , +infty .[ by XXREAL_1: 3;

             not x in { 0 } by d1, TARSKI:def 1;

            hence thesis by XBOOLE_0:def 5, D2;

          end;

          assume

           ASS0: x in (Bor2 \ Bor3);

          then

          reconsider x as Real;

          x in Bor2 & not x in Bor3 by ASS0, XBOOLE_0:def 5;

          then 0 <= x & x < +infty & x <> 0 by TARSKI:def 1, XXREAL_1: 3;

          hence thesis by XXREAL_1: 4;

        end;

        hence thesis by TARSKI: 2;

      end;

      hence thesis;

    end;

    theorem :: FINANCE6:2

    for RV be random_variable of F, Borel_Sets , K be Element of REAL , g2 be Function of Omega, REAL st g2 = ( chi (((RV - (Omega --> K)) " [. 0 , +infty .[),Omega)) holds ( Call-Option (RV,K)) = (g2 (#) (RV - (Omega --> K)))

    proof

      let RV be random_variable of F, Borel_Sets ;

      let K be Element of REAL ;

      let g2 be Function of Omega, REAL ;

      assume

       A2: g2 = ( chi (((RV - (Omega --> K)) " [. 0 , +infty .[),Omega));

      set RVO = (RV - (Omega --> K));

      set CO = ( Call-Option (RV,K));

      

       QQ: ( dom g2) = Omega & ( dom RVO) = Omega & ( dom CO) = Omega by FUNCT_2:def 1;

      

       q1: for c be object st c in ( dom CO) holds (CO . c) = ((g2 . c) * (RVO . c))

      proof

        let c be object;

        assume c in ( dom CO);

        then

        reconsider c as Element of Omega;

        per cases ;

          suppose

           ASSJJ0: c in (RVO " [. 0 , +infty .[);

          then

           ZW0: (g2 . c) = 1 by A2, FUNCT_3:def 3;

          (RVO . c) in [. 0 , +infty .[ by ASSJJ0, FUNCT_1:def 7;

          then 0 <= (RVO . c) & (RVO . c) < +infty by XXREAL_1: 3;

          hence thesis by ZW0, FINANCE3:def 5;

        end;

          suppose

           ASSJJ00: not c in (RVO " [. 0 , +infty .[);

          

           ASSJJ0: c in (RVO " ]. -infty , 0 .[)

          proof

             not (c in ( dom RVO) & (RVO . c) in [. 0 , +infty .[) by FUNCT_1:def 7, ASSJJ00;

            then not c in Omega or not (RVO . c) in [. 0 , +infty .[ by FUNCT_2:def 1;

            then

             T: (RV . c) in ]. -infty , +infty .[ & -infty < (RVO . c) & (RVO . c) < 0 by XXREAL_1: 224, XXREAL_0: 12, XXREAL_0: 9, XXREAL_1: 3;

            (RVO . c) in ]. -infty , 0 .[ by XXREAL_1: 4, T;

            hence thesis by FUNCT_1:def 7, QQ;

          end;

          

           ZW0: (g2 . c) = 0 by A2, ASSJJ00, FUNCT_3:def 3;

          c in ( dom RVO) & (RVO . c) in ]. -infty , 0 .[ by ASSJJ0, FUNCT_1:def 7;

          then -infty < (RVO . c) & (RVO . c) < 0 by XXREAL_1: 4;

          hence thesis by ZW0, FINANCE3:def 5;

        end;

      end;

      for x be object st x in ( dom CO) holds (CO . x) = ((g2 (#) RVO) . x)

      proof

        let x be object;

        assume x in ( dom CO);

        then (CO . x) = ((g2 . x) * (RVO . x)) by q1;

        hence thesis by VALUED_1: 5;

      end;

      hence thesis by QQ;

    end;

    theorem :: FINANCE6:3

    

     TH1: for RV be random_variable of F, Borel_Sets , K be Real holds ((Omega --> K) - RV) is random_variable of F, Borel_Sets

    proof

      let RV be random_variable of F, Borel_Sets , K be Real;

      reconsider K as Element of REAL by XREAL_0:def 1;

      (Omega --> K) is random_variable of F, Borel_Sets by FINANCE3: 10;

      hence thesis by FINANCE2: 24;

    end;

    theorem :: FINANCE6:4

    

     ZZZ: for A be Element of F holds ( chi (A,Omega)) is random_variable of F, Borel_Sets

    proof

      let A be Element of F;

      set chij = ( chi (A,Omega));

      chij is Function & ( rng chij) c= REAL & ( dom chij) = Omega by FUNCT_3:def 3, VALUED_0:def 3;

      then

      reconsider chij2 = chij as Function of Omega, REAL by FUNCT_2: 2;

      reconsider MyOmega = Omega as Element of F by PROB_1: 5;

      chij2 is ( [#] F) -measurable by MESFUNC2: 29;

      then chij2 is Real-Valued-Random-Variable of F by RANDOM_1:def 2;

      hence thesis by RANDOM_3: 7;

    end;

    registration

      let Omega;

      let F;

      cluster F, Borel_Sets -random_variable-like for Function of Omega, REAL ;

      existence

      proof

        set A = the Element of F;

        reconsider c = ( chi (A,Omega)) as Function of Omega, REAL by ZZZ;

        take c;

        thus thesis by ZZZ;

      end;

    end

    theorem :: FINANCE6:5

    

     ChiRandom: ( chi (Omega,Omega)) is F, Borel_Sets -random_variable-like Function of Omega, REAL

    proof

      set g2 = ( chi (Omega,Omega));

      reconsider O = Omega as Element of F by PROB_1: 5;

      ( chi (O,Omega)) is random_variable of F, Borel_Sets by ZZZ;

      hence thesis;

    end;

    theorem :: FINANCE6:6

    

     Lemma00: for f,RV be random_variable of F, Borel_Sets , K be Real holds ((f - RV) " [. 0 , +infty .[) is Element of F

    proof

      let f,RV be random_variable of F, Borel_Sets , K be Real;

      

       A1: [. 0 , +infty .[ is Element of Borel_Sets by FINANCE1: 3;

      (f - RV) is F, Borel_Sets -random_variable-like by FINANCE2: 24;

      hence thesis by A1;

    end;

    

     LemmaRandom: for RV be random_variable of F, Borel_Sets , K be Real holds ( chi (((RV - (Omega --> K)) " [. 0 , +infty .[),Omega)) is random_variable of F, Borel_Sets

    proof

      let RV be random_variable of F, Borel_Sets , K be Real;

      reconsider K as Element of REAL by XREAL_0:def 1;

      (Omega --> K) is random_variable of F, Borel_Sets by FINANCE3: 10;

      then ((RV - (Omega --> K)) " [. 0 , +infty .[) is Element of F by Lemma00;

      hence thesis by ZZZ;

    end;

    definition

      let Omega, F;

      let RV be random_variable of F, Borel_Sets ;

      let K be Real;

      :: original: Call-Option

      redefine

      func Call-Option (RV,K) -> random_variable of F, Borel_Sets ;

      correctness

      proof

        set RVO = (RV - (Omega --> K));

        set g2 = ( chi ((RVO " [. 0 , +infty .[),Omega));

        reconsider g2 as random_variable of F, Borel_Sets by LemmaRandom;

        set RVO = (RV - (Omega --> K));

        reconsider RVO as random_variable of F, Borel_Sets by FINANCE3: 11;

        set CO = ( Call-Option (RV,K));

        CO = (g2 (#) RVO)

        proof

          

           q1: for c be object st c in ( dom CO) holds (CO . c) = ((g2 . c) * (RVO . c))

          proof

            let c be object;

            assume c in ( dom CO);

            then

            reconsider c as Element of Omega;

            (CO . c) = ((g2 . c) * (RVO . c))

            proof

              per cases ;

                suppose

                 ASSJJ0: c in (RVO " [. 0 , +infty .[);

                then

                 ZW0: (g2 . c) = 1 by FUNCT_3:def 3;

                c in ( dom RVO) & (RVO . c) in [. 0 , +infty .[ by ASSJJ0, FUNCT_1:def 7;

                then 0 <= (RVO . c) & (RVO . c) < +infty by XXREAL_1: 3;

                hence thesis by ZW0, FINANCE3:def 5;

              end;

                suppose

                 ASSJJ00: not c in (RVO " [. 0 , +infty .[);

                

                 K1: c in Omega & not c in (RVO " [. 0 , +infty .[) by ASSJJ00;

                

                 ASSJJ0: c in (RVO " ]. -infty , 0 .[)

                proof

                   not (c in ( dom RVO) & (RVO . c) in [. 0 , +infty .[) by ASSJJ00, FUNCT_1:def 7;

                  then not c in Omega or not (RVO . c) in [. 0 , +infty .[ by FUNCT_2:def 1;

                  then (RV . c) in ]. -infty , +infty .[ & -infty < (RVO . c) & (RVO . c) < 0 by XXREAL_1: 224, XXREAL_0: 12, XXREAL_0: 9, XXREAL_1: 3;

                  then c in ( dom RVO) & (RVO . c) in ]. -infty , 0 .[ by K1, FUNCT_2:def 1, XXREAL_1: 4;

                  hence thesis by FUNCT_1:def 7;

                end;

                

                 ZW0: (g2 . c) = 0 by ASSJJ00, FUNCT_3:def 3;

                c in ( dom RVO) & (RVO . c) in ]. -infty , 0 .[ by ASSJJ0, FUNCT_1:def 7;

                then -infty < (RVO . c) & (RVO . c) < 0 by XXREAL_1: 4;

                hence thesis by ZW0, FINANCE3:def 5;

              end;

            end;

            hence thesis;

          end;

          

           W1: ( dom CO) = Omega & ( dom g2) = Omega & ( dom RVO) = Omega by FUNCT_2:def 1;

          for x be object st x in ( dom CO) holds (CO . x) = ((g2 (#) RVO) . x)

          proof

            let x be object;

            assume x in ( dom CO);

            then (CO . x) = ((g2 . x) * (RVO . x)) by q1;

            hence thesis by VALUED_1: 5;

          end;

          hence thesis by W1;

        end;

        hence thesis by FINANCE2: 25;

      end;

    end

    definition

      let Omega, F;

      let RV be random_variable of F, Borel_Sets ;

      let K be Real;

      :: FINANCE6:def1

      func Put-Option (RV,K) -> Function of Omega, REAL means

      : Def30: for w be Element of Omega holds ((((Omega --> K) - RV) . w) >= 0 implies (it . w) = (((Omega --> K) - RV) . w)) & ((((Omega --> K) - RV) . w) < 0 implies (it . w) = 0 );

      existence

      proof

        reconsider MyFunc = ((Omega --> K) - RV) as Function of Omega, REAL ;

        deffunc U( Element of Omega) = ( SetForCall-Option (MyFunc,$1));

        consider f be Function of Omega, REAL such that

         A1: for d be Element of Omega holds (f . d) = U(d) from FUNCT_2:sch 4;

        for w be Element of Omega holds ((MyFunc . w) >= 0 implies (f . w) = (((Omega --> K) - RV) . w)) & ((MyFunc . w) < 0 implies (f . w) = 0 )

        proof

          let w be Element of Omega;

          (f . w) = ( SetForCall-Option (MyFunc,w)) by A1;

          hence thesis by FINANCE3:def 4;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of Omega, REAL ;

        assume that

         A2: for w be Element of Omega holds ((((Omega --> K) - RV) . w) >= 0 implies (f1 . w) = (((Omega --> K) - RV) . w)) & ((((Omega --> K) - RV) . w) < 0 implies (f1 . w) = 0 ) and

         A3: for w be Element of Omega holds ((((Omega --> K) - RV) . w) >= 0 implies (f2 . w) = (((Omega --> K) - RV) . w)) & ((((Omega --> K) - RV) . w) < 0 implies (f2 . w) = 0 );

        let w be Element of Omega;

        per cases ;

          suppose

           A0: (((Omega --> K) - RV) . w) >= 0 ;

          then (f1 . w) = (((Omega --> K) - RV) . w) by A2;

          hence thesis by A0, A3;

        end;

          suppose

           A0: (((Omega --> K) - RV) . w) < 0 ;

          then (f1 . w) = 0 by A2;

          hence thesis by A0, A3;

        end;

      end;

    end

    theorem :: FINANCE6:7

    

     JA3: for RV be random_variable of F, Borel_Sets , K be Real, g2 be Function of Omega, REAL st g2 = ( chi ((((Omega --> K) - RV) " [. 0 , +infty .[),Omega)) holds ( Put-Option (RV,K)) = (g2 (#) ((Omega --> K) - RV))

    proof

      let RV be random_variable of F, Borel_Sets ;

      let K be Real;

      let g2 be Function of Omega, REAL ;

      assume

       K1: g2 = ( chi ((((Omega --> K) - RV) " [. 0 , +infty .[),Omega));

      set PO = ( Put-Option (RV,K));

      set RVO = ((Omega --> K) - RV);

      

       h1: ( dom g2) = Omega & ( dom RVO) = Omega & ( dom PO) = Omega by FUNCT_2:def 1;

      

       q1: ( dom PO) = (( dom g2) /\ ( dom RVO)) & for c be object st c in ( dom PO) holds (PO . c) = ((g2 . c) * (RVO . c))

      proof

        for c be object st c in ( dom PO) holds (PO . c) = ((g2 . c) * (RVO . c))

        proof

          let c be object;

          assume c in ( dom PO);

          then

          reconsider c as Element of Omega;

          (PO . c) = ((g2 . c) * (RVO . c))

          proof

            per cases ;

              suppose

               ASSJJ0: c in (RVO " [. 0 , +infty .[);

              

               ZW0: (g2 . c) = 1 by K1, ASSJJ0, FUNCT_3:def 3;

              c in ( dom RVO) & (RVO . c) in [. 0 , +infty .[ by ASSJJ0, FUNCT_1:def 7;

              then 0 <= (RVO . c) & (RVO . c) < +infty by XXREAL_1: 3;

              hence thesis by ZW0, Def30;

            end;

              suppose

               ASSJJ00: not c in (RVO " [. 0 , +infty .[);

              then

               k1: c in Omega & not c in (RVO " [. 0 , +infty .[);

              

               ASSJJ0: c in (RVO " ]. -infty , 0 .[)

              proof

                 not (c in ( dom RVO) & (RVO . c) in [. 0 , +infty .[) by ASSJJ00, FUNCT_1:def 7;

                then not c in Omega or not (RVO . c) in [. 0 , +infty .[ by FUNCT_2:def 1;

                then (RV . c) in ]. -infty , +infty .[ & -infty < (RVO . c) & (RVO . c) < 0 by XXREAL_1: 224, XXREAL_0: 12, XXREAL_0: 9, XXREAL_1: 3;

                then c in ( dom RVO) & (RVO . c) in ]. -infty , 0 .[ by k1, FUNCT_2:def 1, XXREAL_1: 4;

                hence thesis by FUNCT_1:def 7;

              end;

              

               ZW0: (g2 . c) = 0 by K1, ASSJJ00, FUNCT_3:def 3;

              c in ( dom RVO) & (RVO . c) in ]. -infty , 0 .[ by ASSJJ0, FUNCT_1:def 7;

              then -infty < (RVO . c) & (RVO . c) < 0 by XXREAL_1: 4;

              hence thesis by ZW0, Def30;

            end;

          end;

          hence thesis;

        end;

        hence thesis by h1;

      end;

      for x be object st x in ( dom PO) holds (PO . x) = ((g2 (#) RVO) . x)

      proof

        let x be object;

        assume x in ( dom PO);

        then (PO . x) = ((g2 . x) * (RVO . x)) by q1;

        hence thesis by VALUED_1: 5;

      end;

      hence thesis by h1;

    end;

    definition

      let Omega, F;

      let RV be random_variable of F, Borel_Sets ;

      let K be Real;

      :: original: Put-Option

      redefine

      func Put-Option (RV,K) -> random_variable of F, Borel_Sets ;

      correctness

      proof

        set RVO = ((Omega --> K) - RV);

        set g2 = ( chi ((RVO " [. 0 , +infty .[),Omega));

        set PO = ( Put-Option (RV,K));

        reconsider K as Element of REAL by XREAL_0:def 1;

        (Omega --> K) is random_variable of F, Borel_Sets by FINANCE3: 10;

        then (((Omega --> K) - RV) " [. 0 , +infty .[) is Element of F by Lemma00;

        then

        reconsider g2 as random_variable of F, Borel_Sets by ZZZ;

        reconsider RVO as random_variable of F, Borel_Sets by TH1;

        PO = (g2 (#) RVO) by JA3;

        hence thesis by FINANCE2: 25;

      end;

    end

    begin

    definition

      let Omega, F;

      let RV be random_variable of F, Borel_Sets ;

      let K be Real;

      :: FINANCE6:def2

      func Straddle (RV,K) -> random_variable of F, Borel_Sets equals (( Put-Option (RV,K)) + ( Call-Option (RV,K)));

      coherence by FINANCE2: 23;

    end

    theorem :: FINANCE6:8

    for RV be random_variable of F, Borel_Sets , K be Real holds for w be Element of Omega holds (( Straddle (RV,K)) . w) = |.((RV - (Omega --> K)) . w).|

    proof

      let RV be random_variable of F, Borel_Sets ;

      let K be Real;

      let w be Element of Omega;

      set f1 = RV;

      set f2 = (( - 1) (#) (Omega --> K));

      

       SS: ( dom RV) = Omega & ( dom f2) = Omega by FUNCT_2:def 1;

      then w in (( dom f1) /\ ( dom f2));

      then

       C1: w in ( dom (f1 + f2)) by VALUED_1:def 1;

      ( dom ( Put-Option (RV,K))) = Omega & ( dom ( Call-Option (RV,K))) = Omega by FUNCT_2:def 1;

      then w in (( dom ( Put-Option (RV,K))) /\ ( dom ( Call-Option (RV,K))));

      then

       B100: w in ( dom (( Put-Option (RV,K)) + ( Call-Option (RV,K)))) by VALUED_1:def 1;

      

       c2: ( dom (Omega --> K)) = Omega & ( dom f2) = ( dom (Omega --> K)) by VALUED_1:def 5;

      

       c4: w in ( dom RV) by SS;

      then

       C6: w in ( dom (( - 1) (#) RV)) by VALUED_1:def 5;

      per cases ;

        suppose

         S1: ((RV - (Omega --> K)) . w) > 0 ;

        then

         B0: |.((RV - (Omega --> K)) . w).| = ((RV - (Omega --> K)) . w) by COMPLEX1: 43;

        ( dom ( - RV)) = Omega by FUNCT_2:def 1;

        then w in (( dom (Omega --> K)) /\ ( dom ( - RV)));

        then

         C7: w in ( dom ((Omega --> K) + ( - RV))) by VALUED_1:def 1;

        (((Omega --> K) - RV) . w) < 0

        proof

          ((RV - (Omega --> K)) . w) = ((f1 . w) + (f2 . w)) by C1, VALUED_1:def 1

          .= ((RV . w) + (( - 1) * ((Omega --> K) . w))) by c2, VALUED_1:def 5;

          then ( - ((RV . w) - K)) < 0 by S1;

          then (K - (RV . w)) < 0 ;

          then (((Omega --> K) . w) + (( - 1) * (RV . w))) < 0 ;

          then (((Omega --> K) . w) + ((( - 1) (#) RV) . w)) < 0 by C6, VALUED_1:def 5;

          hence thesis by C7, VALUED_1:def 1;

        end;

        then

         B2: (( Put-Option (RV,K)) . w) = 0 by Def30;

        ((( Put-Option (RV,K)) + ( Call-Option (RV,K))) . w) = ((( Put-Option (RV,K)) . w) + (( Call-Option (RV,K)) . w)) by B100, VALUED_1:def 1;

        hence thesis by B0, B2, FINANCE3:def 5, S1;

      end;

        suppose

         S1: ((RV - (Omega --> K)) . w) < 0 ;

        ( dom ( Put-Option (RV,K))) = Omega & ( dom ( Call-Option (RV,K))) = Omega by FUNCT_2:def 1;

        then w in (( dom ( Put-Option (RV,K))) /\ ( dom ( Call-Option (RV,K))));

        then

         B100: w in ( dom (( Put-Option (RV,K)) + ( Call-Option (RV,K)))) by VALUED_1:def 1;

        

         c2: ( dom (Omega --> K)) = Omega & ( dom f2) = ( dom (Omega --> K)) by VALUED_1:def 5;

        

         C6: w in ( dom (( - 1) (#) RV)) by VALUED_1:def 5, c4;

        ( dom (Omega --> K)) = Omega & ( dom ( - RV)) = Omega by FUNCT_2:def 1;

        then w in (( dom (Omega --> K)) /\ ( dom ( - RV)));

        then

         C7: w in ( dom ((Omega --> K) + ( - RV))) by VALUED_1:def 1;

        (((Omega --> K) - RV) . w) > 0

        proof

          ((RV - (Omega --> K)) . w) = ((f1 . w) + (f2 . w)) by C1, VALUED_1:def 1

          .= ((RV . w) + (( - 1) * ((Omega --> K) . w))) by c2, VALUED_1:def 5;

          then ( - ((RV . w) - K)) > 0 by S1;

          then (K - (RV . w)) > 0 ;

          then (((Omega --> K) . w) + (( - 1) * (RV . w))) > 0 ;

          then (((Omega --> K) . w) + ((( - 1) (#) RV) . w)) > 0 by C6, VALUED_1:def 5;

          hence thesis by C7, VALUED_1:def 1;

        end;

        then

         B2: (( Put-Option (RV,K)) . w) = (((Omega --> K) - RV) . w) by Def30;

        (( Call-Option (RV,K)) . w) = 0 by FINANCE3:def 5, S1;

        then

         B40: (( Straddle (RV,K)) . w) = ( 0 + (((Omega --> K) - RV) . w)) by B2, B100, VALUED_1:def 1;

        ( dom (Omega --> K)) = Omega & ( dom (( - 1) (#) RV)) = Omega by FUNCT_2:def 1;

        then w in (( dom (Omega --> K)) /\ ( dom (( - 1) (#) RV)));

        then w in ( dom ((Omega --> K) + (( - 1) (#) RV))) by VALUED_1:def 1;

        then

         U2: (((Omega --> K) - RV) . w) = (((Omega --> K) . w) + ((( - 1) (#) RV) . w)) by VALUED_1:def 1;

        ( dom (( - 1) (#) RV)) = Omega by FUNCT_2:def 1;

        then

         u3: (((Omega --> K) - RV) . w) = (((Omega --> K) . w) + (( - 1) * (RV . w))) by U2, VALUED_1:def 5;

        

         L1: ((RV . w) + ( - ((Omega --> K) . w))) = ((RV . w) + (( - 1) * ((Omega --> K) . w)));

        ( dom (( - 1) (#) (Omega --> K))) = Omega by FUNCT_2:def 1;

        then

         L2: ((RV . w) + ( - ((Omega --> K) . w))) = ((RV . w) + ((( - 1) (#) (Omega --> K)) . w)) by L1, VALUED_1:def 5;

        w in (( dom RV) /\ ( dom ( - (Omega --> K)))) by SS;

        then w in ( dom (RV + ( - (Omega --> K)))) by VALUED_1:def 1;

        then ((RV . w) + ( - ((Omega --> K) . w))) = ((RV + ( - (Omega --> K))) . w) by L2, VALUED_1:def 1;

        then ( - ((RV - (Omega --> K)) . w)) = (((Omega --> K) - RV) . w) by u3;

        hence thesis by B40, S1, COMPLEX1: 70;

      end;

        suppose

         S1: ((RV - (Omega --> K)) . w) = 0 ;

         0 = (( Straddle (RV,K)) . w)

        proof

          

           H2: ((RV . w) + ((( - 1) (#) (Omega --> K)) . w)) = 0 by VALUED_1: 1, S1;

          ( dom (Omega --> K)) = Omega & ( dom (( - 1) (#) (Omega --> K))) = Omega by FUNCT_2:def 1;

          then

           h1: ((RV . w) + (( - 1) * ((Omega --> K) . w))) = 0 by H2, VALUED_1:def 5;

          ( dom (( - 1) (#) RV)) = Omega by FUNCT_2:def 1;

          then

           G2: (((Omega --> K) . w) + ((( - 1) (#) RV) . w)) = 0 by h1, VALUED_1:def 5;

          ( dom (Omega --> K)) = Omega & ( dom ( - RV)) = Omega by FUNCT_2:def 1;

          then w in (( dom (Omega --> K)) /\ ( dom ( - RV)));

          then w in ( dom ((Omega --> K) + ( - RV))) by VALUED_1:def 1;

          then (((Omega --> K) - RV) . w) = 0 by G2, VALUED_1:def 1;

          then (( Put-Option (RV,K)) . w) = ( - ((RV - (Omega --> K)) . w)) by S1, Def30;

          then

           F3: ((( Call-Option (RV,K)) . w) + (( Put-Option (RV,K)) . w)) = 0 by S1, FINANCE3:def 5;

          ( dom ( Call-Option (RV,K))) = Omega & ( dom ( Put-Option (RV,K))) = Omega by FUNCT_2:def 1;

          then w in (( dom ( Call-Option (RV,K))) /\ ( dom ( Put-Option (RV,K))));

          then w in ( dom (( Call-Option (RV,K)) + ( Put-Option (RV,K)))) by VALUED_1:def 1;

          hence thesis by F3, VALUED_1:def 1;

        end;

        hence thesis by COMPLEX1: 43, S1;

      end;

    end;

    definition

      let Omega, F;

      :: FINANCE6:def3

      func set_of_constant_RV (F) -> set equals { f where f be Function of Omega, REAL : f is random_variable of F, Borel_Sets & f is constant };

      coherence ;

      :: FINANCE6:def4

      func set_of_chi_RV (F) -> set equals { ( chi (A,Omega)) where A be Element of F : ( chi (A,Omega)) is random_variable of F, Borel_Sets };

      coherence ;

    end

    definition

      let Omega, F;

      let X be set;

      :: FINANCE6:def5

      attr X is F -random-membered means

      : RanDef: for x be object st x in X holds x is random_variable of F, Borel_Sets ;

    end

    registration

      let Omega, F;

      cluster ( set_of_constant_RV F) -> non empty;

      coherence

      proof

        set myRV = (Omega --> 0 );

        

         A2: 0 in REAL by NUMBERS: 19;

        reconsider myRV as Function of Omega, REAL by FUNCOP_1: 45, NUMBERS: 19;

        myRV is F, Borel_Sets -random_variable-like by FINANCE3: 10, A2;

        then myRV in ( set_of_constant_RV F);

        hence thesis;

      end;

      cluster ( set_of_chi_RV F) -> non empty;

      coherence

      proof

        reconsider MyOmega = Omega as Element of F by PROB_1: 5;

        set g2 = ( chi (Omega,Omega));

        ( chi (Omega,Omega)) is random_variable of F, Borel_Sets by ChiRandom;

        then ( chi (MyOmega,MyOmega)) in ( set_of_chi_RV F);

        hence thesis;

      end;

    end

    registration

      let Omega, F;

      cluster ( set_of_constant_RV F) -> F -random-membered;

      coherence

      proof

        for x be object st x in ( set_of_constant_RV F) holds x is random_variable of F, Borel_Sets

        proof

          let x be object;

          assume x in ( set_of_constant_RV F);

          then

          consider f be Function of Omega, REAL such that

           A1: x = f & f is random_variable of F, Borel_Sets & f is constant;

          thus thesis by A1;

        end;

        hence thesis;

      end;

      cluster ( set_of_chi_RV F) -> F -random-membered;

      coherence

      proof

        for x be object st x in ( set_of_chi_RV F) holds x is random_variable of F, Borel_Sets

        proof

          let x be object;

          assume x in ( set_of_chi_RV F);

          then

          consider A be Element of F such that

           A1: x = ( chi (A,Omega)) & ( chi (A,Omega)) is random_variable of F, Borel_Sets ;

          thus thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let Omega, F;

      cluster F -random-membered non empty for set;

      existence

      proof

        take ( set_of_constant_RV F);

        thus thesis;

      end;

    end

    definition

      let Omega, F;

      let D be F -random-membered non empty set;

      let ChiFuncs be sequence of D;

      let n be Nat;

      :: FINANCE6:def6

      func Conv_RV (ChiFuncs,n) -> random_variable of F, Borel_Sets equals (ChiFuncs . n);

      coherence by RanDef;

    end

    definition

      let Omega, F;

      let D be F -random-membered non empty set;

      let ConstFuncs be sequence of D;

      let w be Element of Omega;

      :: FINANCE6:def7

      func Conv2_RV (ConstFuncs,w) -> Function of NAT , REAL means

      : Def770: for n be Nat holds (it . n) = (( Conv_RV (ConstFuncs,n)) . w);

      existence

      proof

        deffunc U( Element of NAT ) = (( Conv_RV (ConstFuncs,$1)) . w);

        consider f be Function of NAT , REAL such that

         A1: for d be Element of NAT holds (f . d) = U(d) from FUNCT_2:sch 4;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of NAT , REAL ;

        assume that

         A1: for d be Nat holds (f1 . d) = (( Conv_RV (ConstFuncs,d)) . w) and

         A2: for d be Nat holds (f2 . d) = (( Conv_RV (ConstFuncs,d)) . w);

        let d be Element of NAT ;

        (f2 . d) = (( Conv_RV (ConstFuncs,d)) . w) by A2;

        hence thesis by A1;

      end;

    end

    definition

      let Omega, F;

      let D1,D2 be F -random-membered non empty set;

      let ChiFuncs be sequence of D1;

      let ConstFuncs be sequence of D2;

      let n be Nat;

      :: FINANCE6:def8

      func simple_RV_help (ChiFuncs,ConstFuncs,n) -> Function of Omega, REAL means

      : Def777: for w be Element of Omega holds (it . w) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n);

      existence

      proof

        deffunc U( Element of Omega) = ( In ((( Partial_Sums (( Conv2_RV (ConstFuncs,$1)) (#) ( Conv2_RV (ChiFuncs,$1)))) . n), REAL ));

        consider f be Function of Omega, REAL such that

         A1: for d be Element of Omega holds (f . d) = U(d) from FUNCT_2:sch 4;

        take f;

        let w be Element of Omega;

        ( In ((( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n), REAL )) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n);

        hence thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of Omega, REAL ;

        assume that

         A1: for w be Element of Omega holds (f1 . w) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n) and

         A2: for w be Element of Omega holds (f2 . w) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n);

        let w be Element of Omega;

        (f2 . w) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n) by A2;

        hence thesis by A1;

      end;

    end

    definition

      let Omega, F;

      let D1,D2 be F -random-membered non empty set;

      let ChiFuncs be sequence of D1;

      let ConstFuncs be sequence of D2;

      let n be Nat;

      :: original: simple_RV_help

      redefine

      func simple_RV_help (ChiFuncs,ConstFuncs,n) -> random_variable of F, Borel_Sets ;

      correctness

      proof

        consider f be Function of Omega, REAL such that

         B10: f = ( simple_RV_help (ChiFuncs,ConstFuncs,n));

        f is random_variable of F, Borel_Sets

        proof

          defpred J[ Nat] means ( simple_RV_help (ChiFuncs,ConstFuncs,$1)) is random_variable of F, Borel_Sets ;

          set RVs0 = ( simple_RV_help (ChiFuncs,ConstFuncs, 0 ));

          

           J0: J[ 0 ]

          proof

            for w be Element of Omega holds (RVs0 . w) = ((( Conv_RV (ConstFuncs, 0 )) (#) ( Conv_RV (ChiFuncs, 0 ))) . w)

            proof

              let w be Element of Omega;

              (RVs0 . w) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . 0 ) by Def777;

              then (RVs0 . w) = ((( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w))) . 0 ) by SERIES_1:def 1;

              then

               C2: (RVs0 . w) = ((( Conv2_RV (ConstFuncs,w)) . 0 ) * (( Conv2_RV (ChiFuncs,w)) . 0 )) by VALUED_1: 5;

              

               C3: (( Conv2_RV (ConstFuncs,w)) . 0 ) = (( Conv_RV (ConstFuncs, 0 )) . w) by Def770;

              (( Conv2_RV (ChiFuncs,w)) . 0 ) = (( Conv_RV (ChiFuncs, 0 )) . w) by Def770;

              hence thesis by VALUED_1: 5, C2, C3;

            end;

            then RVs0 = (( Conv_RV (ConstFuncs, 0 )) (#) ( Conv_RV (ChiFuncs, 0 )));

            hence thesis by FINANCE2: 25;

          end;

          

           J1: for n be Nat st J[n] holds J[(n + 1)]

          proof

            let n be Nat;

            assume

             ASS0: J[n];

            set RVsn = ( simple_RV_help (ChiFuncs,ConstFuncs,n));

            set RVsn1 = ( simple_RV_help (ChiFuncs,ConstFuncs,(n + 1)));

            set RVa = (( Conv_RV (ConstFuncs,(n + 1))) (#) ( Conv_RV (ChiFuncs,(n + 1))));

            for w be Element of Omega holds (RVsn1 . w) = ((RVsn + RVa) . w)

            proof

              let w be Element of Omega;

              (RVsn1 . w) = (( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . (n + 1)) by Def777;

              then (RVsn1 . w) = (( In ((( Partial_Sums (( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w)))) . n), REAL )) + ((( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w))) . (n + 1))) by SERIES_1:def 1;

              then (RVsn1 . w) = ((RVsn . w) + ((( Conv2_RV (ConstFuncs,w)) (#) ( Conv2_RV (ChiFuncs,w))) . (n + 1))) by Def777;

              then

               D1: (RVsn1 . w) = ((RVsn . w) + ((( Conv2_RV (ConstFuncs,w)) . (n + 1)) * (( Conv2_RV (ChiFuncs,w)) . (n + 1)))) by VALUED_1: 5;

              

               D2: (( Conv2_RV (ConstFuncs,w)) . (n + 1)) = (( Conv_RV (ConstFuncs,(n + 1))) . w) by Def770;

              (( Conv2_RV (ChiFuncs,w)) . (n + 1)) = (( Conv_RV (ChiFuncs,(n + 1))) . w) by Def770;

              then (RVsn1 . w) = ((RVsn . w) + ((( Conv_RV (ConstFuncs,(n + 1))) (#) ( Conv_RV (ChiFuncs,(n + 1)))) . w)) by VALUED_1: 5, D1, D2;

              hence thesis by VALUED_1: 1;

            end;

            then

             M1: RVsn1 = (RVsn + RVa);

            RVsn is random_variable of F, Borel_Sets & RVa is random_variable of F, Borel_Sets by ASS0, FINANCE2: 25;

            hence thesis by M1, FINANCE2: 23;

          end;

          for k be Nat holds J[k] from NAT_1:sch 2( J0, J1);

          hence thesis by B10;

        end;

        hence thesis by B10;

      end;

    end

    begin

    reserve phi for Real_Sequence;

    reserve jpi for pricefunction;

    

     Lemacik: for x be object holds x in ( set_of_random_variables_on (F, Borel_Sets )) iff x is random_variable of F, Borel_Sets

    proof

      let x be object;

      thus x in ( set_of_random_variables_on (F, Borel_Sets )) implies x is random_variable of F, Borel_Sets

      proof

        assume x in ( set_of_random_variables_on (F, Borel_Sets ));

        then

        consider M be Function of Omega, REAL such that

         AA: x = M & M is F, Borel_Sets -random_variable-like;

        thus x is random_variable of F, Borel_Sets by AA;

      end;

      thus thesis;

    end;

    definition

      let Omega, F;

      let q be Nat;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      :: FINANCE6:def9

      func Change_Element_to_Func (G,q) -> Real-Valued-Random-Variable of F equals (G . q);

      coherence

      proof

        (G . q) is random_variable of F, Borel_Sets by Lemacik;

        hence thesis by RANDOM_3: 7;

      end;

    end

    definition

      let phi, Omega, F;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      let n be Nat;

      :: FINANCE6:def10

      func ArbitrageElSigma1 (phi,Omega,F,G,n) -> Element of F equals (( RVPortfolioValueFutExt (phi,F,G,n)) " [. 0 , +infty .[);

      correctness

      proof

        set RV = ( RVPortfolioValueFutExt (phi,F,G,n));

        

         A1: [. 0 , +infty .[ is Element of Borel_Sets by FINANCE1: 3;

        RV is F, Borel_Sets -random_variable-like by FINANCE3: 6;

        hence thesis by A1;

      end;

      :: FINANCE6:def11

      func ArbitrageElSigma2 (phi,Omega,F,G,n) -> Element of F equals (( RVPortfolioValueFutExt (phi,F,G,n)) " ]. 0 , +infty .[);

      correctness

      proof

        ( RVPortfolioValueFutExt (phi,F,G,n)) is F, Borel_Sets -random_variable-like by FINANCE3: 6;

        hence thesis by A1;

      end;

    end

    definition

      let Omega, F;

      let Prob be Probability of F;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      let jpi be pricefunction;

      let n be Nat;

      :: FINANCE6:def12

      pred Arbitrage_Opportunity_exists_wrt Prob,G,jpi,n means ex phi be Real_Sequence st (( BuyPortfolioExt (phi,jpi,n)) <= 0 & ((Prob . ( ArbitrageElSigma1 (phi,Omega,F,G,n))) = 1 & (Prob . ( ArbitrageElSigma2 (phi,Omega,F,G,n))) > 0 ));

    end

    definition

      let r be Real;

      :: FINANCE6:def13

      func RVfirst (r) -> Element of ( set_of_random_variables_on ( Special_SigmaField1 , Borel_Sets )) equals ( {1, 2, 3, 4} --> r);

      correctness

      proof

        set g = ( {1, 2, 3, 4} --> ( In (r, REAL )));

        g is random_variable of Special_SigmaField1 , Borel_Sets by FINANCE3: 10;

        hence thesis by Lemacik;

      end;

    end

    definition

      let jpi be pricefunction;

      let r be Real;

      let d be Nat;

      :: FINANCE6:def14

      func RVfourth (jpi,r,d) -> Element of ( set_of_random_variables_on ( Special_SigmaField2 , Borel_Sets )) equals ( RVfirst ((jpi . d) * (1 + r)));

      correctness

      proof

        set g = ( {1, 2, 3, 4} --> ( In (((jpi . d) * (1 + r)), REAL )));

        g is random_variable of Special_SigmaField2 , Borel_Sets by FINANCE3: 10;

        then g in { f where f be Function of {1, 2, 3, 4}, REAL : f is Special_SigmaField2 , Borel_Sets -random_variable-like };

        hence thesis;

      end;

    end

    theorem :: FINANCE6:9

    ex G be 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 be Nat st k > 1 holds (G . k) = ( {1, 2, 3, 4} --> 0 ))

    proof

      deffunc U( Nat) = ( IFEQ ($1, 0 ,( RVfirst 1),( IFEQ ($1,1,( RVfirst 5),( RVfirst 0 )))));

      consider f be sequence of ( set_of_random_variables_on ( Special_SigmaField1 , Borel_Sets )) such that

       A1: for d be Element of NAT holds (f . d) = U(d) from FUNCT_2:sch 4;

      take f;

      

       b1: (f . 0 ) = ( IFEQ ( 0 , 0 ,( RVfirst 1),( IFEQ ( 0 ,1,( RVfirst 5),( RVfirst 0 ))))) by A1;

      (f . 1) = ( IFEQ (1, 0 ,( RVfirst 1),( IFEQ (1,1,( RVfirst 5),( RVfirst 0 ))))) by A1;

      then

       b2: (f . 1) = ( IFEQ (1,1,( RVfirst 5),( RVfirst 0 ))) by FUNCOP_1:def 8;

      for k be Nat st k > 1 holds (f . k) = ( {1, 2, 3, 4} --> 0 )

      proof

        let k be Nat;

        assume

         C1: k > 1;

        k in NAT by ORDINAL1:def 12;

        then (f . k) = ( IFEQ (k, 0 ,( RVfirst 1),( IFEQ (k,1,( RVfirst 5),( RVfirst 0 ))))) by A1;

        then (f . k) = ( IFEQ (k,1,( RVfirst 5),( RVfirst 0 ))) by C1, FUNCOP_1:def 8;

        hence thesis by C1, FUNCOP_1:def 8;

      end;

      hence thesis by b1, b2, FUNCOP_1:def 8;

    end;

    theorem :: FINANCE6:10

    for Prob be Probability of Special_SigmaField1 holds for G be 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 be Nat st k > 1 holds (G . k) = ( {1, 2, 3, 4} --> 0 )) holds ex jpi be pricefunction st Arbitrage_Opportunity_exists_wrt (Prob,G,jpi,1)

    proof

      let Prob be Probability of Special_SigmaField1 ;

      set Omega = {1, 2, 3, 4};

      set F = Special_SigmaField1 ;

      let G be sequence of ( set_of_random_variables_on ( Special_SigmaField1 , Borel_Sets ));

      assume

       A3: (G . 0 ) = (Omega --> 1) & (G . 1) = (Omega --> 5) & for k be Nat st k > 1 holds (G . k) = (Omega --> 0 );

      

       ZW: (Prob . Omega) = 1 & (Prob . {} ) = 0

      proof

        (Prob . Omega) = (Prob . ( [#] F));

        then

         B2: (Prob . Omega) = 1 by PROB_1: 30;

        reconsider A = {} as Event of F by PROB_1: 4;

        (Prob . (( [#] F) \ A)) = (Prob . ( [#] F));

        then ((Prob . ( [#] F)) + (Prob . A)) = 1 by PROB_1: 31;

        hence thesis by B2;

      end;

      deffunc U( Element of NAT ) = ( In (( IFEQ ($1, 0 ,1,( IFEQ ($1,1,1, 0 )))), REAL ));

      consider f be Function of NAT , REAL such that

       C1: for d be Element of NAT holds (f . d) = U(d) from FUNCT_2:sch 4;

      f is pricefunction

      proof

        

         d0: (f . 0 ) = U(0) by C1;

        for n be Element of NAT holds (f . n) >= 0

        proof

          let n be Element of NAT ;

          (f . n) = U(n) by C1;

          hence thesis;

        end;

        hence thesis by d0, FINANCE1:def 2, FUNCOP_1:def 8;

      end;

      then

      reconsider jpi = f as pricefunction;

      deffunc U( Element of NAT ) = ( In (( IFEQ ($1, 0 ,( - 1),( IFEQ ($1,1,1, 0 )))), REAL ));

      

       a0: U(0) = ( In (( - 1), REAL )) by FUNCOP_1:def 8

      .= ( - 1);

      

       a1: U() = ( In (( IFEQ (1,1,1, 0 )), REAL )) by FUNCOP_1:def 8

      .= 1 by FUNCOP_1:def 8;

      consider phi be Real_Sequence such that

       A4: for k be Element of NAT holds (phi . k) = U(k) from FUNCT_2:sch 4;

      

       FinJ: ((Prob . ( ArbitrageElSigma1 (phi,Omega,F,G,1))) = 1 & (Prob . ( ArbitrageElSigma2 (phi,Omega,F,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 ) = ( U(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 thesis;

          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) = ( U() * (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 thesis by FUNCOP_1:def 8;

          end;

          hence thesis by H2, H1;

        end;

        set RV = ( RVPortfolioValueFutExt (phi,F,G,1));

        (Prob . ( ArbitrageElSigma1 (phi,Omega,F,G,1))) = 1 & (Prob . ( ArbitrageElSigma2 (phi,Omega,F,G,1))) > 0

        proof

          

           fin1: Omega = (RV " [. 0 , +infty .[)

          proof

            for x be object holds x in Omega iff x in (RV " [. 0 , +infty .[)

            proof

              let x be object;

              x in Omega implies x in (RV " [. 0 , +infty .[)

              proof

                assume x in Omega;

                then

                reconsider x as Element of Omega;

                

                 q1: ( dom RV) = Omega by FUNCT_2:def 1;

                x in ( dom RV) & (RV . x) in [. 0 , +infty .[

                proof

                  set RVh1 = ( RVElementsOfPortfolioValue_fut (phi,F,G, 0 ));

                  (RV . x) = (( RVPortfolioValueFutExt (phi,F,G,( 0 + 1))) . x);

                  then (RV . x) = ((( RVPortfolioValueFut (phi,F,G, 0 )) + ( RVElementsOfPortfolioValue_fut (phi,F,G, 0 ))) . x) by FINANCE3: 9;

                  then

                   S0: (RV . x) = ((( RVPortfolioValueFut (phi,F,G, 0 )) . x) + (RVh1 . x)) by VALUED_1: 1;

                   0 <= (RV . x) & (RV . x) < +infty

                  proof

                    

                     S1: (RVh1 . x) = ( - 1)

                    proof

                      (RVh1 . x) = ((( ElementsOfPortfolioValueProb_fut (F,(G . 0 ))) . x) * (phi . 0 )) by FINANCE2:def 5;

                      then

                       K1: (RVh1 . x) = ((( Change_Element_to_Func (F, Borel_Sets ,(G . 0 ))) . x) * (phi . 0 )) by FINANCE1:def 8;

                      set G0 = (G . 0 );

                      

                       K2: G0 = ( Change_Element_to_Func (F, Borel_Sets ,(G . 0 ))) by FINANCE1:def 7;

                      reconsider G0 as Function of Omega, REAL by K1, FINANCE1:def 7;

                      (RVh1 . x) = (1 * (phi . 0 )) by A3, K1, K2;

                      

                      then (RVh1 . x) = (1 * U(0)) by A4

                      .= ( In (( - 1), REAL )) by FUNCOP_1:def 8;

                      hence thesis;

                    end;

                    set RV0 = ( RVPortfolioValueFut (phi,F,G, 0 ));

                    (RV0 . x) = 5

                    proof

                      (RV0 . x) = ( PortfolioValueFut (( 0 + 1),phi,F,G,x)) by FINANCE3:def 3;

                      then (RV0 . x) = ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . 0 ) by SERIES_1:def 1;

                      then (RV0 . x) = (( ElementsOfPortfolioValue_fut (phi,F,x,G)) . ( 0 + 1)) by NAT_1:def 3;

                      then (RV0 . x) = ((( ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (phi . 1)) by FINANCE1:def 10;

                      then (RV0 . x) = ((( ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * U()) by A4;

                      then

                       R1: (RV0 . x) = ((( Change_Element_to_Func (F, Borel_Sets ,(G . 1))) . x) * 1) by a1, FINANCE1:def 8;

                      (G . 1) = ( Change_Element_to_Func (F, Borel_Sets ,(G . 1))) by FINANCE1:def 7;

                      then

                      reconsider G1 = (G . 1) as Function of Omega, REAL ;

                      (RV0 . x) = ((G1 . x) * 1) by R1, FINANCE1:def 7;

                      hence thesis by A3;

                    end;

                    hence thesis by XXREAL_0: 9, S0, S1;

                  end;

                  hence thesis by q1, XXREAL_1: 3;

                end;

                hence thesis by FUNCT_1:def 7;

              end;

              hence thesis;

            end;

            hence thesis by TARSKI: 2;

          end;

          Omega = (RV " ]. 0 , +infty .[)

          proof

            for x be object holds x in Omega iff x in (RV " ]. 0 , +infty .[)

            proof

              let x be object;

              thus x in Omega implies x in (RV " ]. 0 , +infty .[)

              proof

                assume x in Omega;

                then

                reconsider x as Element of Omega;

                

                 q1: ( dom RV) = Omega by FUNCT_2:def 1;

                x in ( dom RV) & (RV . x) in ]. 0 , +infty .[

                proof

                  set RVh1 = ( RVElementsOfPortfolioValue_fut (phi,F,G, 0 ));

                  (RV . x) = (( RVPortfolioValueFutExt (phi,F,G,( 0 + 1))) . x);

                  then (RV . x) = ((( RVPortfolioValueFut (phi,F,G, 0 )) + ( RVElementsOfPortfolioValue_fut (phi,F,G, 0 ))) . x) by FINANCE3: 9;

                  then

                   S0: (RV . x) = ((( RVPortfolioValueFut (phi,F,G, 0 )) . x) + (RVh1 . x)) by VALUED_1: 1;

                   0 < (RV . x) & (RV . x) < +infty

                  proof

                    (RVh1 . x) = ((( ElementsOfPortfolioValueProb_fut (F,(G . 0 ))) . x) * (phi . 0 )) by FINANCE2:def 5;

                    then

                     K1: (RVh1 . x) = ((( Change_Element_to_Func (F, Borel_Sets ,(G . 0 ))) . x) * (phi . 0 )) by FINANCE1:def 8;

                    set G0 = (G . 0 );

                    

                     K2: G0 = ( Change_Element_to_Func (F, Borel_Sets ,(G . 0 ))) by FINANCE1:def 7;

                    reconsider G0 as Function of Omega, REAL by K1, FINANCE1:def 7;

                    (RVh1 . x) = (1 * (phi . 0 )) by A3, K1, K2;

                    then

                     S1: (RVh1 . x) = ( - 1) by a0, A4;

                    set RV0 = ( RVPortfolioValueFut (phi,F,G, 0 ));

                    (RV0 . x) = ( PortfolioValueFut (( 0 + 1),phi,F,G,x)) by FINANCE3:def 3;

                    then (RV0 . x) = ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . 0 ) by SERIES_1:def 1;

                    then (RV0 . x) = (( ElementsOfPortfolioValue_fut (phi,F,x,G)) . ( 0 + 1)) by NAT_1:def 3;

                    then (RV0 . x) = ((( ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * (phi . 1)) by FINANCE1:def 10;

                    then (RV0 . x) = ((( ElementsOfPortfolioValueProb_fut (F,(G . 1))) . x) * U()) by A4;

                    then

                     R1: (RV0 . x) = ((( Change_Element_to_Func (F, Borel_Sets ,(G . 1))) . x) * 1) by a1, FINANCE1:def 8;

                    (G . 1) = ( Change_Element_to_Func (F, Borel_Sets ,(G . 1))) by FINANCE1:def 7;

                    then

                    reconsider G1 = (G . 1) as Function of Omega, REAL ;

                    (RV0 . x) = ((G1 . x) * 1) by R1, FINANCE1:def 7;

                    then (RV0 . x) = 5 by A3;

                    hence thesis by XXREAL_0: 9, S0, S1;

                  end;

                  hence thesis by q1, XXREAL_1: 4;

                end;

                hence thesis by FUNCT_1:def 7;

              end;

              thus thesis;

            end;

            hence thesis by TARSKI: 2;

          end;

          hence thesis by fin1, ZW;

        end;

        hence thesis by G1;

      end;

      take jpi;

      thus thesis by FinJ;

    end;

    theorem :: FINANCE6:11

    

     JB1: for n be Nat holds for r be Real holds for G be sequence of ( set_of_random_variables_on (F, Borel_Sets )) holds { w where w be Element of Omega : ( PortfolioValueFutExt (n,phi,F,G,w)) >= 0 } = (( RVPortfolioValueFutExt (phi,F,G,n)) " [. 0 , +infty .[)

    proof

      let d be Nat;

      let r be Real;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      set Set1 = { w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) >= 0 };

      set Set2 = (( RVPortfolioValueFutExt (phi,F,G,d)) " [. 0 , +infty .[);

      for x be object holds x in Set1 iff x in Set2

      proof

        let x be object;

        thus x in Set1 implies x in Set2

        proof

          assume x in Set1;

          then

          consider w be Element of Omega such that

           A1: w = x & ( PortfolioValueFutExt (d,phi,F,G,w)) >= 0 ;

          ( PortfolioValueFutExt (d,phi,F,G,w)) = (( RVPortfolioValueFutExt (phi,F,G,d)) . w) by FINANCE3:def 1;

          then

           A2: (( RVPortfolioValueFutExt (phi,F,G,d)) . w) in [. 0 , +infty .[ by XXREAL_1: 3, A1, XXREAL_0: 9;

          ( dom ( RVPortfolioValueFutExt (phi,F,G,d))) = Omega by FUNCT_2:def 1;

          hence thesis by A1, A2, FUNCT_1:def 7;

        end;

        assume

         a1: x in Set2;

        then

         A1: x in ( dom ( RVPortfolioValueFutExt (phi,F,G,d))) & (( RVPortfolioValueFutExt (phi,F,G,d)) . x) in [. 0 , +infty .[ by FUNCT_1:def 7;

        reconsider x as Element of Omega by a1;

         0 <= (( RVPortfolioValueFutExt (phi,F,G,d)) . x) & (( RVPortfolioValueFutExt (phi,F,G,d)) . x) < +infty by A1, XXREAL_1: 3;

        then 0 <= ( PortfolioValueFutExt (d,phi,F,G,x)) by FINANCE3:def 1;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINANCE6:12

    

     JB2: for d,d2 be Nat st d2 = (d - 1) holds for r be Real holds for G be sequence of ( set_of_random_variables_on (F, Borel_Sets )) holds { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) >= ((1 + r) * ( BuyPortfolio (phi,jpi,d))) } = ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) " [. 0 , +infty .[)

    proof

      let d,d2 be Nat;

      assume

       a10: d2 = (d - 1);

      let r be Real;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      set Set1 = { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) >= ((1 + r) * ( BuyPortfolio (phi,jpi,d))) };

      set Set2 = ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) " [. 0 , +infty .[);

      for x be object holds x in Set1 iff x in Set2

      proof

        let x be object;

        thus x in Set1 implies x in Set2

        proof

          assume x in Set1;

          then

          consider w be Element of Omega such that

           A1: w = x & ( PortfolioValueFut (d,phi,F,G,w)) >= ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

          reconsider x as Element of Omega by A1;

          set myel = ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

          

           a2: ( PortfolioValueFut ((d2 + 1),phi,F,G,w)) = (( RVPortfolioValueFut (phi,F,G,d2)) . w) by FINANCE3:def 3;

          ((( RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> myel) . x)) >= 0 by XREAL_1: 48, A1, a2, a10;

          then

           Q1: ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + (( - 1) * ((Omega --> myel) . x))) >= 0 ;

          x in ( dom (Omega --> myel));

          then x in ( dom (( - 1) (#) (Omega --> myel))) by VALUED_1:def 5;

          then ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + ((( - 1) (#) (Omega --> myel)) . x)) >= 0 by Q1, VALUED_1:def 5;

          then ((( RVPortfolioValueFut (phi,F,G,d2)) + ( - (Omega --> myel))) . x) >= 0 by VALUED_1: 1;

          then

           T1: ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> myel)) . x) in [. 0 , +infty .[ by XXREAL_1: 3, XXREAL_0: 9;

          ( dom (( RVPortfolioValueFut (phi,F,G,d2)) + ( - (Omega --> myel)))) = (Omega /\ Omega) by FUNCT_2:def 1;

          hence thesis by T1, FUNCT_1:def 7;

        end;

        assume

         a1: x in Set2;

        then

         A1: x in ( dom (( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d)))))) & ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) . x) in [. 0 , +infty .[ by FUNCT_1:def 7;

        set my1 = ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

        set my2 = (( RVPortfolioValueFut (phi,F,G,d2)) . x);

        reconsider x as Element of Omega by a1;

        set RVmyx = ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) . x);

        RVmyx = ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + ((( - 1) (#) (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) . x)) by VALUED_1: 1;

        then RVmyx = ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + (( - 1) * ((Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) . x))) by VALUED_1: 6;

        then 0 <= ((( RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) . x)) by A1, XXREAL_1: 3;

        then 0 <= (my2 - my1);

        then ( 0 + my1) <= my2 by XREAL_1: 19;

        then ((1 + r) * ( BuyPortfolio (phi,jpi,d))) <= ( PortfolioValueFut ((d2 + 1),phi,F,G,x)) by FINANCE3:def 3;

        hence thesis by a10;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINANCE6:13

    

     JB3: for d,d2 be Nat holds for r be Real holds for G be sequence of ( set_of_random_variables_on (F, Borel_Sets )) holds ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) " [. 0 , +infty .[) is Event of F

    proof

      let d,d2 be Nat;

      let r be Real;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      set RV = ( RVPortfolioValueFut (phi,F,G,d2));

      reconsider RV as random_variable of F, Borel_Sets by FINANCE3: 7;

      set myr = ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

      reconsider myr as Element of REAL by XREAL_0:def 1;

      reconsider constRV = (Omega --> myr) as random_variable of F, Borel_Sets by FINANCE3: 10;

      

       B5: [. 0 , +infty .[ is Element of Borel_Sets by FINANCE1: 3;

      (RV - constRV) is F, Borel_Sets -random_variable-like by FINANCE2: 24;

      hence thesis by B5;

    end;

    theorem :: FINANCE6:14

    

     JC1: for d be Nat holds for r be Real holds for G be sequence of ( set_of_random_variables_on (F, Borel_Sets )) holds { w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) > 0 } = (( RVPortfolioValueFutExt (phi,F,G,d)) " ]. 0 , +infty .[)

    proof

      let d be Nat;

      let r be Real;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      set Set1 = { w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) > 0 };

      set Set2 = (( RVPortfolioValueFutExt (phi,F,G,d)) " ]. 0 , +infty .[);

      for x be object holds x in Set1 iff x in Set2

      proof

        let x be object;

        thus x in Set1 implies x in Set2

        proof

          assume x in Set1;

          then

          consider w be Element of Omega such that

           A1: w = x & ( PortfolioValueFutExt (d,phi,F,G,w)) > 0 ;

          reconsider x as Element of Omega by A1;

           0 < (( RVPortfolioValueFutExt (phi,F,G,d)) . w) & (( RVPortfolioValueFutExt (phi,F,G,d)) . w) < +infty by A1, XXREAL_0: 9, FINANCE3:def 1;

          then

           A2: (( RVPortfolioValueFutExt (phi,F,G,d)) . w) in ]. 0 , +infty .[ by XXREAL_1: 4;

          ( dom ( RVPortfolioValueFutExt (phi,F,G,d))) = Omega by FUNCT_2:def 1;

          hence thesis by A1, A2, FUNCT_1:def 7;

        end;

        assume

         a1: x in Set2;

        then

         A1: x in ( dom ( RVPortfolioValueFutExt (phi,F,G,d))) & (( RVPortfolioValueFutExt (phi,F,G,d)) . x) in ]. 0 , +infty .[ by FUNCT_1:def 7;

        reconsider x as Element of Omega by a1;

         0 < (( RVPortfolioValueFutExt (phi,F,G,d)) . x) & (( RVPortfolioValueFutExt (phi,F,G,d)) . x) < +infty by A1, XXREAL_1: 4;

        then 0 < ( PortfolioValueFutExt (d,phi,F,G,x)) by FINANCE3:def 1;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINANCE6:15

    

     JC2: for d,d2 be Nat st d2 = (d - 1) holds for r be Real holds for G be sequence of ( set_of_random_variables_on (F, Borel_Sets )) holds { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) > ((1 + r) * ( BuyPortfolio (phi,jpi,d))) } = ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) " ]. 0 , +infty .[)

    proof

      let d,d2 be Nat;

      assume

       a10: d2 = (d - 1);

      let r be Real;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      set Set1 = { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) > ((1 + r) * ( BuyPortfolio (phi,jpi,d))) };

      set Set2 = ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) " ]. 0 , +infty .[);

      for x be object holds x in Set1 iff x in Set2

      proof

        let x be object;

        thus x in Set1 implies x in Set2

        proof

          assume x in Set1;

          then

          consider w be Element of Omega such that

           A1: w = x & ( PortfolioValueFut (d,phi,F,G,w)) > ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

          reconsider x as Element of Omega by A1;

          set myel = ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

          

           a2: ( PortfolioValueFut ((d2 + 1),phi,F,G,w)) = (( RVPortfolioValueFut (phi,F,G,d2)) . w) by FINANCE3:def 3;

          ((( RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> myel) . x)) > 0 by XREAL_1: 50, A1, a2, a10;

          then

           Q1: ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + (( - 1) * ((Omega --> myel) . x))) > 0 ;

          x in ( dom (Omega --> myel));

          then x in ( dom (( - 1) (#) (Omega --> myel))) by VALUED_1:def 5;

          then ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + ((( - 1) (#) (Omega --> myel)) . x)) > 0 by Q1, VALUED_1:def 5;

          then 0 < ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> myel)) . x) & ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> myel)) . x) < +infty by XXREAL_0: 9, VALUED_1: 1;

          then

           T1: ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> myel)) . x) in ]. 0 , +infty .[ by XXREAL_1: 4;

          ( dom (( RVPortfolioValueFut (phi,F,G,d2)) + ( - (Omega --> myel)))) = (Omega /\ Omega) by FUNCT_2:def 1;

          hence thesis by T1, FUNCT_1:def 7;

        end;

        assume

         a1: x in Set2;

        then

         A1: x in ( dom (( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d)))))) & ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) . x) in ]. 0 , +infty .[ by FUNCT_1:def 7;

        set my1 = ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

        set my2 = (( RVPortfolioValueFut (phi,F,G,d2)) . x);

        reconsider x as Element of Omega by a1;

        set RVmyx = ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) . x);

        RVmyx = ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + ((( - 1) (#) (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) . x)) by VALUED_1: 1;

        then RVmyx = ((( RVPortfolioValueFut (phi,F,G,d2)) . x) + (( - 1) * ((Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) . x))) by VALUED_1: 6;

        then 0 < ((( RVPortfolioValueFut (phi,F,G,d2)) . x) - ((Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) . x)) by A1, XXREAL_1: 4;

        then 0 < (my2 - my1);

        then ( 0 + my1) < ((my2 - my1) + my1) by XREAL_1: 6;

        then ((1 + r) * ( BuyPortfolio (phi,jpi,d))) < ( PortfolioValueFut ((d2 + 1),phi,F,G,x)) by FINANCE3:def 3;

        hence thesis by a10;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     ZZ: ( [. 0 , +infty .[ \ { 0 }) = ]. 0 , +infty .[ by XXREAL_1: 136;

    theorem :: FINANCE6:16

    

     JC3: for d,d2 be Nat holds for r be Real holds for G be sequence of ( set_of_random_variables_on (F, Borel_Sets )) holds ((( RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * ( BuyPortfolio (phi,jpi,d))))) " ]. 0 , +infty .[) is Event of F

    proof

      let d,d2 be Nat;

      let r be Real;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

       { 0 } is Element of Borel_Sets & [. 0 , +infty .[ is Element of Borel_Sets by FINANCE1: 3, FINANCE2: 5;

      then

       B1: ]. 0 , +infty .[ is Element of Borel_Sets by PROB_1: 6, ZZ;

      set RV = ( RVPortfolioValueFut (phi,F,G,d2));

      reconsider RV as random_variable of F, Borel_Sets by FINANCE3: 7;

      set myr = ((1 + r) * ( BuyPortfolio (phi,jpi,d)));

      reconsider myr as Element of REAL by XREAL_0:def 1;

      set constRV = (Omega --> myr);

      reconsider constRV as random_variable of F, Borel_Sets by FINANCE3: 10;

      (RV - constRV) is F, Borel_Sets -random_variable-like by FINANCE2: 24;

      hence thesis by B1;

    end;

    theorem :: FINANCE6:17

    for jpi be pricefunction holds for d,d2 be Nat st d > 0 & d2 = (d - 1) holds for Prob be Probability of F holds for r be Real st r > ( - 1) holds for G be 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 be 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 ))

    proof

      let jpi be pricefunction;

      let d,d2 be Nat;

      assume

       A1: d > 0 & d2 = (d - 1);

      let Prob be Probability of F;

      let r be Real;

      assume

       A2: r > ( - 1);

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      assume

       A3: ( Element_Of (F, Borel_Sets ,G, 0 )) = (Omega --> (1 + r));

      thus ( Arbitrage_Opportunity_exists_wrt (Prob,G,jpi,d)) implies (ex myphi be 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 ))

      proof

        assume Arbitrage_Opportunity_exists_wrt (Prob,G,jpi,d);

        then

        consider phi be 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 be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) >= 0 } by JB1;

        then ( ArbitrageElSigma1 (phi,Omega,F,G,d)) c= { w where w be 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 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 be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) > 0 } by JC1;

        then ( ArbitrageElSigma2 (phi,Omega,F,G,d)) c= { w where w be 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 as Event of F by JC3;

        (Prob . ( ArbitrageElSigma2 (phi,Omega,F,G,d))) <= (Prob . RVspec2) by C3, PROB_1: 34;

        hence thesis by Fin1, C1;

      end;

      given myphi be 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 ;

      deffunc U( Nat) = ( In (( IFEQ ($1, 0 ,( - ( BuyPortfolio (myphi,jpi,d))),(myphi . $1))), REAL ));

      consider phi be Real_Sequence such that

       AA1: for n be Element of NAT holds (phi . n) = U(n) from FUNCT_2:sch 4;

      

       AA10: for n be Nat holds (n = 0 implies (phi . n) = ( - ( BuyPortfolio (myphi,jpi,d)))) & (n > 0 implies (phi . n) = (myphi . n))

      proof

        let n be Nat;

        

         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 ;

            suppose n = 0 ;

            then ( IFEQ (n, 0 ,( - ( BuyPortfolio (myphi,jpi,d))),(myphi . n))) = ( - ( BuyPortfolio (myphi,jpi,d))) by FUNCOP_1:def 8;

            hence thesis by XREAL_0:def 1;

          end;

            suppose n <> 0 ;

            hence thesis by FUNCOP_1:def 8, SU;

          end;

        end;

        hereby

          assume

           SQ: n = 0 ;

          

          then (phi . n) = U(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;

        end;

        assume

         SQ: n > 0 ;

        (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 thesis by FUNCOP_1:def 8, SQ;

      end;

      set B0 = ( - ( BuyPortfolio (myphi,jpi,d)));

      

       Z1: ( BuyPortfolioExt (phi,jpi,d)) = 0

      proof

        ( BuyPortfolioExt (phi,jpi,d)) = (B0 + ( 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 Pr[ Nat] means (P1 . $1) = (P2 . $1);

              

               J0: Pr[ 0 ]

              proof

                (P1 . 0 ) = ((( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . 0 ) by SERIES_1:def 1;

                then (P1 . 0 ) = (( ElementsOfBuyPortfolio (phi,jpi)) . ( 0 + 1)) by NAT_1:def 3;

                then

                 Erg1: (P1 . 0 ) = ((phi . 1) * (jpi . 1)) by VALUED_1: 5;

                (P2 . 0 ) = ((( ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1) . 0 ) by SERIES_1:def 1;

                then (P2 . 0 ) = (( ElementsOfBuyPortfolio (myphi,jpi)) . ( 0 + 1)) by NAT_1:def 3;

                then (P2 . 0 ) = ((myphi . 1) * (jpi . 1)) by VALUED_1: 5;

                hence thesis by Erg1, AA10;

              end;

              

               J1: for n be Nat st Pr[n] holds Pr[(n + 1)]

              proof

                let n be Nat;

                assume

                 f1: Pr[n];

                (P1 . (n + 1)) = ((P1 . n) + ((( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (n + 1))) by SERIES_1:def 1;

                then (P1 . (n + 1)) = ((P1 . n) + (( ElementsOfBuyPortfolio (phi,jpi)) . ((n + 1) + 1))) by NAT_1:def 3;

                then

                 Erg1: (P1 . (n + 1)) = ((P1 . n) + ((phi . (n + 2)) * (jpi . (n + 2)))) by VALUED_1: 5;

                set n2 = (n + 2);

                (P2 . (n + 1)) = ((P2 . n) + ((( ElementsOfBuyPortfolio (myphi,jpi)) ^\ 1) . (n + 1))) by SERIES_1:def 1;

                then (P2 . (n + 1)) = ((P2 . n) + (( ElementsOfBuyPortfolio (myphi,jpi)) . ((n + 1) + 1))) by NAT_1:def 3;

                then (P2 . (n + 1)) = ((P2 . n) + ((myphi . n2) * (jpi . n2))) by VALUED_1: 5;

                hence thesis by Erg1, f1, AA10;

              end;

              for n be Nat holds Pr[n] from NAT_1:sch 2( J0, J1);

              hence thesis by A1;

            end;

            hence thesis;

          end;

          hence thesis by zw, AA10;

        end;

        hence thesis;

      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)))));

        (Set1 " [. 0 , +infty .[) = (Set2 " [. 0 , +infty .[)

        proof

          for x be object holds x in (Set1 " [. 0 , +infty .[) iff x in (Set2 " [. 0 , +infty .[)

          proof

            let x be object;

            thus x in (Set1 " [. 0 , +infty .[) implies x in (Set2 " [. 0 , +infty .[)

            proof

              assume

               sc: x in (Set1 " [. 0 , +infty .[);

              then

              reconsider x as Element of Omega;

              (Set1 . 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 Set2) & (Set2 . 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 J[ Nat] means (( Partial_Sums (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1) = (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1);

                  

                   K1: J[ 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 thesis by SERIES_1:def 1;

                  end;

                  

                   K2: for n be Nat st J[n] holds J[(n + 1)]

                  proof

                    let n be Nat;

                    assume

                     AK2: J[n];

                    set n1 = (n + 1);

                    set n2 = (n1 + 1);

                    

                     R: (( Partial_Sums (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . n1) = ((( 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 . n2))) . x) * (myphi . n2)) 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) . n1) = ((( ElementsOfPortfolioValueProb_fut (F,(G . n2))) . x) * (phi . n2)) by R1, AA10;

                      then ((( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . n1) = (( ElementsOfPortfolioValue_fut (phi,F,x,G)) . (n1 + 1)) by FINANCE1:def 10;

                      hence thesis by NAT_1:def 3;

                    end;

                    hence thesis by SERIES_1:def 1, R;

                  end;

                  for n be Nat holds J[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 thesis by FINANCE3:def 3;

                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 thesis;

                end;

                hence thesis by UUU, VALUED_1: 13;

              end;

              hence thesis by FUNCT_1:def 7;

            end;

            assume

             ab: x in (Set2 " [. 0 , +infty .[);

            then

             ABC1: x in ( dom Set2) & (Set2 . x) in [. 0 , +infty .[ by FUNCT_1:def 7;

            reconsider 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 thesis by AA10;

            end;

            then

             ABC4: (( PortfolioValueFut ((d2 + 1),myphi,F,G,x)) + ((1 + r) * (phi . 0 ))) in [. 0 , +infty .[ by FINANCE3:def 3, ABC3;

            

             ABC2: (Set1 . 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 J[ Nat] means (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1) = (( Partial_Sums (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1);

                  

                   K1: J[ 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 thesis by SERIES_1:def 1;

                  end;

                  

                   K2: for n be Nat st J[n] holds J[(n + 1)]

                  proof

                    let n be Nat;

                    set n1 = (n + 1);

                    set n2 = (n1 + 1);

                    assume J[n];

                    then

                     R: (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . n1) = ((( 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) . n1) = ((( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . n1)

                    proof

                      ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . n1) = (( ElementsOfPortfolioValue_fut (phi,F,x,G)) . (n1 + 1)) by NAT_1:def 3;

                      then

                       QA: ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . n1) = ((( ElementsOfPortfolioValueProb_fut (F,(G . n2))) . x) * (phi . n2)) by FINANCE1:def 10;

                      (phi . n2) = (myphi . n2) by AA10;

                      then ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . n1) = (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) . n2) by FINANCE1:def 10, QA;

                      hence thesis by NAT_1:def 3;

                    end;

                    hence thesis by SERIES_1:def 1, R;

                  end;

                  for n be Nat holds J[n] from NAT_1:sch 2( K1, K2);

                  hence thesis;

                end;

                hence thesis;

              end;

              then ( PortfolioValueFutExt ((d2 + 1),phi,F,G,x)) in [. 0 , +infty .[ by A3, FINANCE1: 12, ABC4;

              hence thesis by A1, FINANCE3:def 1;

            end;

            ( dom Set1) = Omega by FUNCT_2:def 1;

            hence thesis by FUNCT_1:def 7, ABC2;

          end;

          hence thesis by TARSKI: 2;

        end;

        hence thesis by ASS0;

      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 be object holds x in (Set1 " ]. 0 , +infty .[) iff x in (Set2 " ]. 0 , +infty .[)

          proof

            let x be object;

            thus x in (Set1 " ]. 0 , +infty .[) implies x in (Set2 " ]. 0 , +infty .[)

            proof

              assume

               ss: x in (Set1 " ]. 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 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 Set2) & (Set2 . x) in ]. 0 , +infty .[

              proof

                (( RVPortfolioValueFut (myphi,F,G,d2)) . x) = (( RVPortfolioValueFut (phi,F,G,d2)) . x)

                proof

                  defpred J[ Nat] means (( Partial_Sums (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . $1) = (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . $1);

                  

                   K1: J[ 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 thesis by SERIES_1:def 1;

                  end;

                  

                   K2: for n be Nat st J[n] holds J[(n + 1)]

                  proof

                    let n be Nat;

                    assume

                     AK2: J[n];

                    set n1 = (n + 1);

                    set n2 = (n1 + 1);

                    

                     R: (( Partial_Sums (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1)) . n1) = ((( 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 . n2))) . x) * (myphi . n2)) by FINANCE1:def 10;

                      ((( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . n1) = ((( ElementsOfPortfolioValueProb_fut (F,(G . n2))) . x) * (phi . n2)) by R1, AA10;

                      then ((( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . n1) = (( ElementsOfPortfolioValue_fut (phi,F,x,G)) . (n1 + 1)) by FINANCE1:def 10;

                      hence thesis by NAT_1:def 3;

                    end;

                    hence thesis by SERIES_1:def 1, R;

                  end;

                  for n be Nat holds J[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 thesis by FINANCE3:def 3;

                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 thesis;

                end;

                hence thesis by UUU, VALUED_1: 13;

              end;

              hence thesis by FUNCT_1:def 7;

            end;

            assume

             ab: x in (Set2 " ]. 0 , +infty .[);

            then

             ABC1: x in ( dom Set2) & (Set2 . x) in ]. 0 , +infty .[ by FUNCT_1:def 7;

            reconsider 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: (Set1 . 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 J[ 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: J[ 0 ]

                  proof

                    (( 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 thesis by SERIES_1:def 1;

                  end;

                  

                   K2: for n be Nat st J[n] holds J[(n + 1)]

                  proof

                    let n be Nat;

                    set n1 = (n + 1);

                    set n2 = (n1 + 1);

                    assume J[n];

                    then

                     R: (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1)) . n1) = ((( 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) . n1) = ((( ElementsOfPortfolioValue_fut (myphi,F,x,G)) ^\ 1) . n1)

                    proof

                      ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . n1) = (( ElementsOfPortfolioValue_fut (phi,F,x,G)) . (n1 + 1)) by NAT_1:def 3;

                      then

                       QA: ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . n1) = ((( ElementsOfPortfolioValueProb_fut (F,(G . n2))) . x) * (phi . n2)) by FINANCE1:def 10;

                      (phi . n2) = (myphi . n2) by AA10;

                      then ((( ElementsOfPortfolioValue_fut (phi,F,x,G)) ^\ 1) . n1) = (( ElementsOfPortfolioValue_fut (myphi,F,x,G)) . (n1 + 1)) by FINANCE1:def 10, QA;

                      hence thesis by NAT_1:def 3;

                    end;

                    hence thesis by SERIES_1:def 1, R;

                  end;

                  for n be Nat holds J[n] from NAT_1:sch 2( K1, K2);

                  hence thesis;

                end;

                hence thesis;

              end;

              then ( PortfolioValueFutExt ((d2 + 1),phi,F,G,x)) in ]. 0 , +infty .[ by A3, FINANCE1: 12, ABC4;

              hence thesis by A1, FINANCE3:def 1;

            end;

            ( dom Set1) = Omega by FUNCT_2:def 1;

            hence thesis by FUNCT_1:def 7, ABC2;

          end;

          hence thesis by TARSKI: 2;

        end;

        hence thesis by ASS0;

      end;

      hence thesis by Z1, Z2;

    end;

    begin

    definition

      let Omega, F;

      let RV be Real-Valued-Random-Variable of F;

      let r be Real;

      :: FINANCE6:def15

      func Real_RV (r,RV) -> Real-Valued-Random-Variable of F equals (RV (#) (1 / (1 + r)));

      correctness

      proof

        ((1 / (1 + r)) (#) RV) is random_variable of F, Borel_Sets by RANDOM_3: 7;

        hence thesis;

      end;

    end

    definition

      let Omega, F;

      let jpi be pricefunction;

      let G be sequence of ( set_of_random_variables_on (F, Borel_Sets ));

      let r be Real;

      :: FINANCE6:def16

      pred Risk_neutral_measure_exists_wrt G,jpi,r means ex Prob be Probability of F st for d be Nat holds (jpi . d) = ( expect (( Real_RV (r,( Change_Element_to_Func (G,d)))),Prob));

    end

    reserve Prob for Probability of Special_SigmaField2 ;

    theorem :: FINANCE6:18

    

     ThArbPrel: for r be Real st r > 0 holds for jpi be pricefunction holds for d be Nat holds ex f be Real-Valued-Random-Variable of Special_SigmaField2 st f = ( {1, 2, 3, 4} --> ((jpi . d) * (1 + r))) & f is_integrable_on ( P2M Prob) & f is_simple_func_in Special_SigmaField2

    proof

      set F2 = Special_SigmaField2 ;

      set Omega2 = {1, 2, 3, 4};

      let r be Real;

      assume

       ASSJ: r > 0 ;

      let jpi be pricefunction;

      let d be Nat;

      deffunc U( Element of Omega2) = ( In (((jpi . d) * (1 + r)), REAL ));

      consider f be Function of Omega2, REAL such that

       A1: for d be Element of Omega2 holds (f . d) = U(d) from FUNCT_2:sch 4;

      set g = (Omega2 --> ( In (((jpi . d) * (1 + r)), REAL )));

      

       b1: ( dom f) = Omega2 & ( dom g) = Omega2 by FUNCT_2:def 1;

      

       AA: d in NAT by ORDINAL1:def 12;

      for x be object st x in ( dom f) holds (f . x) = (g . x)

      proof

        let x be object;

        assume x in ( dom f);

        then

        reconsider x as Element of Omega2;

        (f . x) = ( In (((jpi . d) * (1 + r)), REAL )) by A1;

        hence thesis;

      end;

      then

       ff: f = g by b1;

      then

      reconsider f as Real-Valued-Random-Variable of F2 by FINANCE3: 10, RANDOM_3: 7;

      

       zz: Omega2 in F2 & ( dom ( R_EAL f)) = Omega2 by PROB_1: 5, FUNCT_2:def 1;

      for x be object st x in ( dom f) holds (( R_EAL f) . x) = ( In (((jpi . d) * (1 + r)), REAL )) by ff, FUNCOP_1: 7;

      then

       Fin3: f is_simple_func_in F2 by MESFUNC6: 2, zz, MESFUNC6: 49;

      reconsider g = f as random_variable of F2, Borel_Sets by ff, FINANCE3: 10;

      reconsider fREAL = ( R_EAL f) as random_variable of F2, Borel_Sets by ff, FINANCE3: 10;

      reconsider FOmega = {1, 2, 3, 4} as Element of F2 by PROB_1: 5;

      

       Q1: FOmega = ( dom ( R_EAL f)) by FUNCT_2:def 1;

      f is_integrable_on ( P2M Prob)

      proof

        ( R_EAL f) is_integrable_on ( P2M Prob)

        proof

          ( R_EAL f) is FOmega -measurable & ( integral+ (( P2M Prob),( max+ ( R_EAL f)))) < +infty & ( integral+ (( P2M Prob),( max- ( R_EAL f)))) < +infty

          proof

            

             Q2: ( R_EAL f) is FOmega -measurable

            proof

              for r be Real holds (FOmega /\ ( less_dom (( R_EAL f),r))) in F2

              proof

                let r be Real;

                set WX = { w where w be Element of Omega2 : (fREAL . w) < r };

                

                 W1: (FOmega /\ ( less_dom (fREAL,r))) = WX

                proof

                  for x be object holds x in (FOmega /\ ( less_dom (fREAL,r))) iff x in WX

                  proof

                    let x be object;

                    thus x in (FOmega /\ ( less_dom (fREAL,r))) implies x in WX

                    proof

                      assume x in (FOmega /\ ( less_dom (fREAL,r)));

                      then x in FOmega & x in ( less_dom (fREAL,r)) by XBOOLE_0:def 4;

                      then x in FOmega & (x in ( dom fREAL) & (fREAL . x) < r) by MESFUNC1:def 11;

                      hence thesis;

                    end;

                    assume x in WX;

                    then x in ( less_dom (fREAL,r)) by FINANCE1: 9;

                    then x in ( dom fREAL) & (fREAL . x) < r by MESFUNC1:def 11;

                    then x in FOmega & x in ( less_dom (fREAL,r)) by MESFUNC1:def 11;

                    hence thesis by XBOOLE_0:def 4;

                  end;

                  hence thesis by TARSKI: 2;

                end;

                WX = (g " ]. -infty , r.[) in F2

                proof

                  

                   qq1: for x be object holds x in WX iff x in (g " ]. -infty , r.[)

                  proof

                    let x be object;

                    thus x in WX implies x in (g " ]. -infty , r.[)

                    proof

                      assume x in WX;

                      then

                      consider w be Element of Omega2 such that

                       YA1: w = x & (fREAL . w) < r;

                      reconsider x as Element of Omega2 by YA1;

                       -infty < (fREAL . x) & (fREAL . x) < r by XXREAL_0: 12, YA1;

                      then (g . x) in ]. -infty , r.[ & ( dom g) = Omega2 by FUNCT_2:def 1, XXREAL_1: 4;

                      hence thesis by FUNCT_1:def 7;

                    end;

                    assume

                     c0: x in (g " ]. -infty , r.[);

                    then

                     C0: x in ( dom g) & (g . x) in ]. -infty , r.[ by FUNCT_1:def 7;

                    reconsider x as Element of Omega2 by c0;

                     -infty < (g . x) & (g . x) < r & (g . x) = (fREAL . x) by C0, XXREAL_1: 4;

                    hence thesis;

                  end;

                  

                   ZZ: ]. -infty , r.[ is Element of Borel_Sets & g is random_variable of F2, Borel_Sets by FINANCE1: 3;

                  g is F2, Borel_Sets -random_variable-like;

                  hence thesis by qq1, TARSKI: 2, ZZ;

                end;

                hence thesis by W1;

              end;

              hence thesis by MESFUNC1:def 16;

            end;

            set fREAL = ( R_EAL f);

            set maxfREAL = ( max+ fREAL);

            

             U0: ( dom maxfREAL) = ( dom fREAL) & ( dom fREAL) = Omega2 by MESFUNC2:def 2, FUNCT_2:def 1;

            

             Fin30: maxfREAL is nonnegative

            proof

              for x be ExtReal holds x in ( rng maxfREAL) implies 0. <= x

              proof

                let x be ExtReal;

                assume

                 CASS0: x in ( rng maxfREAL);

                consider w be object such that

                 W1: w in ( dom maxfREAL) & (maxfREAL . w) = x by CASS0, FUNCT_1:def 3;

                thus thesis by W1, MESFUNC2: 12;

              end;

              hence thesis by SUPINF_2:def 12, SUPINF_2:def 9;

            end;

            ( integral+ (( P2M Prob),( max+ ( R_EAL f)))) < +infty & ( integral+ (( P2M Prob),( max- ( R_EAL f)))) < +infty

            proof

              maxfREAL is_simple_func_in F2

              proof

                for x be object st x in ( dom maxfREAL) holds (maxfREAL . x) = ( In (((jpi . d) * (1 + r)), REAL ))

                proof

                  let x be object;

                  assume x in ( dom maxfREAL);

                  then

                  reconsider x as Element of Omega2;

                  per cases ;

                    suppose 0 <= (fREAL . x);

                    then

                     S2: ( max ((fREAL . x), 0 )) = (fREAL . x) by XXREAL_0:def 10;

                    (fREAL . x) = ( In (((jpi . d) * (1 + r)), REAL )) by ff;

                    hence thesis by U0, MESFUNC2:def 2, S2;

                  end;

                    suppose

                     S1: 0 > (fREAL . x);

                     0 < (1 + r) & 0 <= (jpi . d) by AA, FINANCE1:def 2, ASSJ;

                    hence thesis by S1, ff;

                  end;

                end;

                hence thesis by MESFUNC6: 2, U0, PROB_1: 5;

              end;

              then

               Schritt1: ( integral+ (( P2M Prob),( max+ fREAL))) = ( integral' (( P2M Prob),( max+ fREAL))) by MESFUNC5: 77, Fin30;

              reconsider myr = ((jpi . d) * (1 + r)) as Element of REAL by XREAL_0:def 1;

              ( dom ( max+ fREAL)) = ( dom fREAL) by MESFUNC2:def 2;

              then

               y1: ( dom ( max+ fREAL)) = ( [#] Special_SigmaField2 ) by FUNCT_2:def 1;

              

               y2: 0 < (1 + r) & 0 <= (jpi . d) by AA, FINANCE1:def 2, ASSJ;

              

               zz1: for x be object st x in ( dom ( max+ fREAL)) holds (( max+ fREAL) . x) = myr

              proof

                let x be object;

                assume

                 S: x in ( dom ( max+ fREAL));

                then

                reconsider x as Element of Omega2;

                

                 YY1: (( max+ fREAL) . x) = ( max ((fREAL . x), 0 )) by MESFUNC2:def 2, S;

                per cases ;

                  suppose (fREAL . x) >= 0 ;

                  then (( max+ fREAL) . x) = (fREAL . x) by YY1, XXREAL_0:def 10;

                  hence thesis by A1;

                end;

                  suppose (fREAL . x) < 0 ;

                  hence thesis by A1, y2;

                end;

              end;

              (( P2M Prob) . ( dom ( max+ fREAL))) = 1

              proof

                ( dom ( max+ fREAL)) = ( dom fREAL) by MESFUNC2:def 2;

                then ( dom ( max+ fREAL)) = ( [#] Special_SigmaField2 ) by FUNCT_2:def 1;

                hence thesis by PROB_1: 30;

              end;

              then

               fin1: ( integral+ (( P2M Prob),( max+ fREAL))) = (myr * 1) by zz1, Schritt1, MESFUNC5: 104, y2, y1;

              set maxmfREAL = ( max- fREAL);

              

               YY: ( dom maxmfREAL) = ( dom fREAL) & ( dom fREAL) = Omega2 by MESFUNC2:def 3, FUNCT_2:def 1;

              

               JFin1: maxmfREAL is nonnegative

              proof

                for x be ExtReal holds x in ( rng maxmfREAL) implies 0. <= x

                proof

                  let x be ExtReal;

                  assume x in ( rng maxmfREAL);

                  then ex w be object st w in ( dom maxmfREAL) & (maxmfREAL . w) = x by FUNCT_1:def 3;

                  hence thesis by MESFUNC2: 13;

                end;

                hence thesis by SUPINF_2:def 12, SUPINF_2:def 9;

              end;

              

               U1: ( dom maxmfREAL) in F2 by PROB_1: 5, YY;

              ( integral+ (( P2M Prob),( max- fREAL))) < +infty

              proof

                

                 FFF: for x be object st x in ( dom maxmfREAL) holds (maxmfREAL . x) = 0

                proof

                  let x be object;

                  assume x in ( dom maxmfREAL);

                  then

                  reconsider x as Element of Omega2;

                  

                   QQQ1: ( - (fREAL . x)) = ( - ((jpi . d) * (1 + r))) by A1;

                  set mfREAL = ( - (fREAL . x));

                   0 < (1 + r) & 0 <= (jpi . d) by AA, FINANCE1:def 2, ASSJ;

                  then

                   QQQ3: ( max (( - (fREAL . x)), 0 )) = 0 by XXREAL_0:def 10, QQQ1;

                  ( dom ( max- fREAL)) = ( dom fREAL) & ( dom fREAL) = Omega2 by MESFUNC2:def 3, FUNCT_2:def 1;

                  hence thesis by QQQ3, MESFUNC2:def 3;

                end;

                then

                 Schritt1: ( integral+ (( P2M Prob),( max- fREAL))) = ( integral' (( P2M Prob),( max- fREAL))) by MESFUNC5: 77, JFin1, MESFUNC6: 2, U1;

                

                 aq2: ( dom maxmfREAL) = ( dom fREAL) & ( dom fREAL) = Omega2 by MESFUNC2:def 3, FUNCT_2:def 1;

                ( integral+ (( P2M Prob),( max- fREAL))) = ( 0 * (( P2M Prob) . ( dom ( max- fREAL)))) by Schritt1, MESFUNC5: 104, aq2, FFF, PROB_1: 5;

                hence thesis;

              end;

              hence thesis by fin1, XXREAL_0: 9;

            end;

            hence thesis by Q2;

          end;

          hence thesis by Q1;

        end;

        hence thesis;

      end;

      hence thesis by ff, Fin3;

    end;

    theorem :: FINANCE6:19

    

     ThArb: for n be Nat holds for r be Real st r > 0 holds for jpi be pricefunction holds for d be Nat holds for RV be Real-Valued-Random-Variable of Special_SigmaField2 st RV = ( {1, 2, 3, 4} --> ((jpi . d) * (1 + r))) & RV is_integrable_on ( P2M Prob) & RV is_simple_func_in Special_SigmaField2 holds (jpi . d) = ( expect (( Real_RV (r,RV)),Prob))

    proof

      let n be Nat;

      set Omega2 = {1, 2, 3, 4};

      set F2 = Special_SigmaField2 ;

      let r be Real;

      assume

       A00: r > 0 ;

      let jpi be pricefunction;

      let d be Nat;

      let RV be Real-Valued-Random-Variable of F2;

      assume

       ASS0: RV = (Omega2 --> ((jpi . d) * (1 + r))) & RV is_integrable_on ( P2M Prob) & RV is_simple_func_in F2;

      set myconst = (1 / (1 + r));

      

       Z1: ( expect (( Real_RV (r,RV)),Prob)) = (myconst * ( expect (RV,Prob))) by ASS0, RANDOM_1:def 3, RANDOM_1: 27;

      

       B1: ( expect (RV,Prob)) = ( Integral (( P2M Prob),RV)) by ASS0, RANDOM_1:def 3, RANDOM_1:def 4;

      reconsider FOmega = Omega2 as Element of F2 by PROB_1: 5;

      

       D1: FOmega = ( dom RV) by FUNCT_2:def 1;

      

       SS: ( R_EAL RV) = RV & RV is nonnegative

      proof

        for x be ExtReal holds x in ( rng RV) implies 0. <= x

        proof

          let x be ExtReal;

          assume

           CASS0: x in ( rng RV);

          consider w be object such that

           W1: w in ( dom RV) & (RV . w) = x by CASS0, FUNCT_1:def 3;

          reconsider w as Element of Omega2 by W1;

           0 <= (RV . w)

          proof

            d in NAT by ORDINAL1:def 12;

            then 0 <= (jpi . d) by FINANCE1:def 2;

            hence thesis by ASS0, A00;

          end;

          hence thesis by W1;

        end;

        hence thesis by SUPINF_2:def 12, SUPINF_2:def 9;

      end;

      then ( expect (RV,Prob)) = ( integral+ (( P2M Prob),( R_EAL RV))) by D1, ASS0, MESFUNC6: 50, B1, MESFUNC6: 82;

      then

       Q3: ( expect (RV,Prob)) = ( integral' (( P2M Prob),( R_EAL RV))) by MESFUNC5: 77, MESFUNC6: 49, ASS0, SS;

      set myr = ((jpi . d) * (1 + r));

      d in NAT by ORDINAL1:def 12;

      then

       TT: 0 <= (jpi . d) by FINANCE1:def 2;

      (for x be object st x in ( dom ( R_EAL RV)) holds (( R_EAL RV) . x) = myr) & ( dom ( R_EAL RV)) in F2 & 0 <= myr by ASS0, FUNCOP_1: 7, TT, A00, PROB_1: 5;

      then

       Q4: ( expect (RV,Prob)) = (myr * (( P2M Prob) . ( dom ( R_EAL RV)))) by Q3, MESFUNC5: 104;

      ( dom ( R_EAL RV)) = Omega2 & Omega2 = ( [#] F2) by FUNCT_2:def 1;

      then ( expect (RV,Prob)) = (myr * 1) by Q4, PROB_1: 30;

      then

       Spec: ( expect (( Real_RV (r,RV)),Prob)) = ((jpi . d) * ((1 / (1 + r)) * (1 + r))) by Z1;

      1 = ((1 * (1 + r)) * ((1 + r) " )) by XCMPLX_1: 203, A00;

      hence thesis by Spec;

    end;

    theorem :: FINANCE6:20

    for r be Real st r > 0 holds for jpi be pricefunction holds ex G be sequence of ( set_of_random_variables_on ( Special_SigmaField2 , Borel_Sets )) st (for d be Nat holds (G . d) = ( {1, 2, 3, 4} --> ((jpi . d) * (1 + r))) & ( Change_Element_to_Func (G,d)) is_integrable_on ( P2M Prob) & ( Change_Element_to_Func (G,d)) is_simple_func_in Special_SigmaField2 )

    proof

      let r be Real;

      assume

       A1: r > 0 ;

      let jpi be pricefunction;

      deffunc U( Nat) = ( RVfourth (jpi,r,$1));

      consider g be sequence of ( set_of_random_variables_on ( Special_SigmaField2 , Borel_Sets )) such that

       A2: for d be Element of NAT holds (g . d) = U(d) from FUNCT_2:sch 4;

      take g;

      let d be Nat;

      d in NAT by ORDINAL1:def 12;

      then

       b1: ( Change_Element_to_Func (g,d)) = ( RVfourth (jpi,r,d)) by A2;

      ex RV be Real-Valued-Random-Variable of Special_SigmaField2 st RV = ( {1, 2, 3, 4} --> ( In (((jpi . d) * (1 + r)), REAL ))) & RV is_integrable_on ( P2M Prob) & RV is_simple_func_in Special_SigmaField2 by A1, ThArbPrel;

      hence thesis by b1;

    end;

    theorem :: FINANCE6:21

    for r be Real st r > 0 holds for jpi be pricefunction holds for G be sequence of ( set_of_random_variables_on ( Special_SigmaField2 , Borel_Sets )) st for d be Nat holds (G . d) = ( {1, 2, 3, 4} --> ((jpi . d) * (1 + r))) & ( Change_Element_to_Func (G,d)) is_integrable_on ( P2M Prob) & ( Change_Element_to_Func (G,d)) is_simple_func_in Special_SigmaField2 holds ( Risk_neutral_measure_exists_wrt (G,jpi,r) & for s be Nat holds (jpi . s) = ( expect (( Real_RV (r,( Change_Element_to_Func (G,s)))),Prob)))

    proof

      let r be Real;

      assume

       A0: r > 0 ;

      let jpi be pricefunction;

      let G be sequence of ( set_of_random_variables_on ( Special_SigmaField2 , Borel_Sets ));

      assume

       A01: for d be Nat holds (G . d) = ( {1, 2, 3, 4} --> ((jpi . d) * (1 + r))) & ( Change_Element_to_Func (G,d)) is_integrable_on ( P2M Prob) & ( Change_Element_to_Func (G,d)) is_simple_func_in Special_SigmaField2 ;

      for s be Nat holds (jpi . s) = ( expect (( Real_RV (r,( Change_Element_to_Func (G,s)))),Prob))

      proof

        let s be Nat;

        set RV = ( Change_Element_to_Func (G,s));

        RV = ( {1, 2, 3, 4} --> ( In (((jpi . s) * (1 + r)), REAL ))) & RV is_integrable_on ( P2M Prob) & RV is_simple_func_in Special_SigmaField2 by A01;

        hence thesis by A0, ThArb;

      end;

      hence thesis;

    end;