finance1.miz



    begin

    reserve Omega,Omega2 for non empty set;

    reserve Sigma,F for SigmaField of Omega;

    reserve Sigma2,F2 for SigmaField of Omega2;

    notation

      let a,r be Real;

      synonym halfline_fin (a,r) for [.a,r.[;

    end

    definition

      let a,r be Real;

      :: original: halfline_fin

      redefine

      func halfline_fin (a,r) -> Subset of REAL ;

      coherence

      proof

        ( halfline_fin (a,r)) = [.a, r.[;

        hence thesis;

      end;

    end

    theorem :: FINANCE1:1

    for k be Real holds ( REAL \ [.k, +infty .[) = ]. -infty , k.[

    proof

      let k be Real;

      

       A1: k in REAL by XREAL_0:def 1;

      for x be object holds x in ( REAL \ [.k, +infty .[) iff x in ]. -infty , k.[

      proof

        let x be object;

        hereby

          assume

           A2: x in ( REAL \ [.k, +infty .[);

          

           A3: x in ]. -infty , +infty .[ & not x in [.k, +infty .[ by A2, XBOOLE_0:def 5, XXREAL_1: 224;

          consider y be Element of REAL such that

           A4: x = y by A2;

          y in ]. -infty , +infty .[ & not y >= k by A4, A3, XXREAL_1: 236;

          hence x in ]. -infty , k.[ by A4, XXREAL_1: 233;

        end;

        assume

         A5: x in ]. -infty , k.[;

        then k in REAL & x in ]. -infty , k.[ & x in { a where a be Element of ExtREAL : -infty < a & a < k } by XREAL_0:def 1, XXREAL_1:def 4;

        then

        consider a be Element of ExtREAL such that

         A6: a = x & -infty < a & a < k;

        consider y be Element of ExtREAL such that

         A7: x = y by A6;

        reconsider y as Element of REAL by A1, A6, A7, XXREAL_0: 47;

        y < k by A5, A7, XXREAL_1: 233;

        then y in REAL & not y in [.k, +infty .[ by XXREAL_1: 236;

        hence thesis by A7, XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINANCE1:2

    

     Th2: for k be Real holds ( REAL \ ]. -infty , k.[) = [.k, +infty .[

    proof

      let k be Real;

      

       A1: k in REAL by XREAL_0:def 1;

      for x be object holds x in ( REAL \ ]. -infty , k.[) iff x in [.k, +infty .[

      proof

        let x be object;

        hereby

          assume

           A2: x in ( REAL \ ]. -infty , k.[);

          

           A3: x in ]. -infty , +infty .[ & not x in ]. -infty , k.[ by A2, XBOOLE_0:def 5, XXREAL_1: 224;

          consider y be Element of REAL such that

           A4: x = y by A2;

          

           A5: y in ]. -infty , +infty .[ & not y < k by A4, A3, XXREAL_1: 233;

          thus x in [.k, +infty .[ by A5, A4, XXREAL_1: 236;

        end;

        assume

         A6: x in [.k, +infty .[;

        then k in REAL & x in [.k, +infty .[ & x in { a where a be Element of ExtREAL : k <= a & a < +infty } by XREAL_0:def 1, XXREAL_1:def 2;

        then

        consider a be Element of ExtREAL such that

         A7: a = x & k <= a & a < +infty ;

        consider y be Element of ExtREAL such that

         A8: x = y by A7;

        reconsider y as Element of REAL by A7, A8, A1, XXREAL_0: 46;

        y >= k by A6, A8, XXREAL_1: 236;

        then y in REAL & not y in ]. -infty , k.[ by XXREAL_1: 233;

        hence thesis by A8, XBOOLE_0:def 5;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let a,b be Real;

      :: FINANCE1:def1

      func half_open_sets (a,b) -> SetSequence of REAL means

      : Def1: (it . 0 ) = ( halfline_fin (a,(b + 1))) & for n be Nat holds (it . (n + 1)) = ( halfline_fin (a,(b + (1 / (n + 1)))));

      existence

      proof

        defpred P[ set, set, set] means for x,y be Subset of REAL , s be Nat holds s = $1 & x = $2 & y = $3 implies y = ( halfline_fin (a,(b + (1 / (s + 1)))));

        

         A1: for n be Nat holds for x be Subset of REAL holds ex y be Subset of REAL st P[n, x, y]

        proof

          let n be Nat;

          let x be Subset of REAL ;

          take ( halfline_fin (a,(b + (1 / (n + 1)))));

          thus thesis;

        end;

        consider F be SetSequence of REAL such that

         A2: (F . 0 ) = ( halfline_fin (a,(b + 1))) and

         A3: for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A1);

        take F;

        thus (F . 0 ) = ( halfline_fin (a,(b + 1))) by A2;

        let n be Nat;

        reconsider n as Element of NAT by ORDINAL1:def 12;

         P[n, (F . n), (F . (n + 1))] by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be SetSequence of REAL such that

         A4: (S1 . 0 ) = ( halfline_fin (a,(b + 1))) & for n be Nat holds (S1 . (n + 1)) = ( halfline_fin (a,(b + (1 / (n + 1))))) and

         A5: (S2 . 0 ) = ( halfline_fin (a,(b + 1))) & for n be Nat holds (S2 . (n + 1)) = ( halfline_fin (a,(b + (1 / (n + 1)))));

        defpred P[ object] means (S1 . $1) = (S2 . $1);

        for n be object holds n in NAT implies P[n]

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n as Element of NAT ;

          

           A6: P[ 0 ] by A4, A5;

          

           A7: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume (S1 . k) = (S2 . k);

            

            thus (S1 . (k + 1)) = ( halfline_fin (a,(b + (1 / (k + 1))))) by A4

            .= (S2 . (k + 1)) by A5;

          end;

          for k be Nat holds P[k] from NAT_1:sch 2( A6, A7);

          then (S1 . n) = (S2 . n);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      :: FINANCE1:def2

      mode pricefunction -> Real_Sequence means

      : Def2: (it . 0 ) = 1 & for n be Element of NAT holds (it . n) >= 0 ;

      existence

      proof

        reconsider j = 1 as Element of REAL by XREAL_0:def 1;

        take ( NAT --> j);

        thus thesis by FUNCOP_1: 7;

      end;

    end

    notation

      let phi,jpi be Real_Sequence;

      synonym ElementsOfBuyPortfolio (phi,jpi) for phi (#) jpi;

    end

    definition

      let phi,jpi be Real_Sequence;

      :: original: ElementsOfBuyPortfolio

      redefine

      func ElementsOfBuyPortfolio (phi,jpi) -> Real_Sequence ;

      coherence

      proof

        ( ElementsOfBuyPortfolio (phi,jpi)) = (phi (#) jpi);

        hence thesis;

      end;

    end

    definition

      let d be Nat;

      let phi,jpi be Real_Sequence;

      :: FINANCE1:def3

      func BuyPortfolioExt (phi,jpi,d) -> Real equals (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . d);

      coherence ;

      :: FINANCE1:def4

      func BuyPortfolio (phi,jpi,d) -> Real equals (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1));

      coherence ;

    end

    definition

      let Omega,Omega2 be set;

      let Sigma be SigmaField of Omega;

      let Sigma2 be SigmaField of Omega2;

      let X be Function of Omega, Omega2;

      :: FINANCE1:def5

      attr X is Sigma,Sigma2 -random_variable-like means for x be set st x in Sigma2 holds (X " x) in Sigma;

    end

    

     Lm1: for Omega,Omega2 be non empty set, F be Function of Omega, Omega2, y be non empty set holds { z where z be Element of Omega : (F . z) is Element of y } = (F " y)

    proof

      let Omega,Omega2 be non empty set, F be Function of Omega, Omega2, y be non empty set;

      set D = { z where z be Element of Omega : (F . z) is Element of y };

      for x be object holds x in D iff x in (F " y)

      proof

        let x be object;

        hereby

          assume x in D;

          then

          consider z be Element of Omega such that

           A1: x = z & (F . z) is Element of y;

          z in Omega;

          then

           A2: z in ( dom F) by FUNCT_2:def 1;

          (F . z) in y by A1;

          then z in (F " y) by FUNCT_1:def 7, A2;

          hence x in (F " y) by A1;

        end;

        assume x in (F " y);

        then

         A3: x in ( dom F) & (F . x) in y by FUNCT_1:def 7;

        thus x in D by A3;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     LemmaExample: for f be Function of Omega, Omega2 st f = (Omega --> the Element of Omega2) holds f is F, F2 -random_variable-like

    proof

      set k = the Element of Omega2;

      set z = (Omega --> k);

      z is F, F2 -random_variable-like iff (for x be set st x in F2 holds (z " x) in F);

      for x be Element of F2 holds (z " x) in F

      proof

        let x be Element of F2;

        set K = (z " x);

        

         A2: ( dom z) = Omega by FUNCT_2:def 1;

        per cases ;

          suppose

           A3: k in x;

          for s be object holds s in K iff s in Omega

          proof

            let s be object;

            thus s in K implies s in Omega;

            assume s in Omega;

            then s in Omega & (z . s) in x by A3, FUNCOP_1: 7;

            hence thesis by A2, FUNCT_1:def 7;

          end;

          then K = Omega by TARSKI: 2;

          then K is Element of F by PROB_1: 23;

          hence thesis;

        end;

          suppose

           A4: not k in x;

          for r be object holds not r in K

          proof

            let r be object;

            assume r in K;

            then r in ( dom z) & (z . r) in x by FUNCT_1:def 7;

            hence thesis by A4, FUNCOP_1: 7;

          end;

          then K = {} by XBOOLE_0:def 1;

          hence thesis by PROB_1: 4;

        end;

      end;

      hence thesis;

    end;

    registration

      let Omega1,Omega2 be non empty set;

      let S1 be SigmaField of Omega1;

      let S2 be SigmaField of Omega2;

      cluster S1, S2 -random_variable-like for Function of Omega1, Omega2;

      existence

      proof

        set f = (Omega1 --> the Element of Omega2);

        reconsider f as Function of Omega1, Omega2;

        take f;

        thus thesis by LemmaExample;

      end;

    end

    definition

      let Omega,Omega2 be non empty set;

      let F be SigmaField of Omega;

      let F2 be SigmaField of Omega2;

      mode random_variable of F,F2 is F, F2 -random_variable-like Function of Omega, Omega2;

    end

    definition

      let Omega,Omega2 be set;

      let F be SigmaField of Omega;

      let F2 be SigmaField of Omega2;

      :: FINANCE1:def6

      func set_of_random_variables_on (F,F2) -> set equals { M where M be Function of Omega, Omega2 : M is F, F2 -random_variable-like };

      coherence ;

    end

    registration

      let Omega, Omega2, F, F2;

      cluster ( set_of_random_variables_on (F,F2)) -> non empty;

      coherence

      proof

        set X = ( set_of_random_variables_on (F,F2));

        ex z be Function of Omega, Omega2 st z is F, F2 -random_variable-like

        proof

          set k = the Element of Omega2;

          set z = (Omega --> k);

          

           A1: z is F, F2 -random_variable-like iff (for x be set st x in F2 holds (z " x) in F);

          for x be Element of F2 holds (z " x) in F

          proof

            let x be Element of F2;

            set K = (z " x);

            

             A2: ( dom z) = Omega by FUNCT_2:def 1;

            per cases ;

              suppose

               A3: k in x;

              for s be object holds s in K iff s in Omega

              proof

                let s be object;

                thus s in K implies s in Omega;

                assume s in Omega;

                then s in Omega & (z . s) in x by A3, FUNCOP_1: 7;

                hence thesis by A2, FUNCT_1:def 7;

              end;

              then K = Omega by TARSKI: 2;

              then K is Element of F by PROB_1: 23;

              hence thesis;

            end;

              suppose

               A4: not k in x;

              for r be object holds not r in K

              proof

                let r be object;

                assume r in K;

                then r in ( dom z) & (z . r) in x by FUNCT_1:def 7;

                hence thesis by A4, FUNCOP_1: 7;

              end;

              then K = {} by XBOOLE_0:def 1;

              hence thesis by PROB_1: 4;

            end;

          end;

          hence thesis by A1;

        end;

        then

        consider z be Function of Omega, Omega2 such that

         A5: z is F, F2 -random_variable-like;

        z in X by A5;

        hence thesis;

      end;

    end

    registration

      let Omega, Omega2, F, F2;

      cluster ( set_of_random_variables_on (F,F2)) -> functional;

      coherence

      proof

        let x be object;

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

        then

        consider z be Function of Omega, Omega2 such that

         A5: z = x & z is F, F2 -random_variable-like;

        x is Function by A5;

        hence thesis;

      end;

    end

    definition

      let Omega,Omega2 be non empty set;

      let F be SigmaField of Omega;

      let F2 be SigmaField of Omega2;

      let X be set;

      let k be Element of X;

      :: FINANCE1:def7

      func Change_Element_to_Func (F,F2,k) -> Function of Omega, Omega2 equals

      : Def7: k;

      coherence

      proof

        k in X by A1;

        then ex f be Function of Omega, Omega2 st f = k & f is F, F2 -random_variable-like by A1;

        hence thesis;

      end;

    end

    definition

      let Omega be non empty set;

      let F be SigmaField of Omega;

      let X be non empty set;

      let k be Element of X;

      :: FINANCE1:def8

      func ElementsOfPortfolioValueProb_fut (F,k) -> Function of Omega, REAL means

      : Def8: for w be Element of Omega holds (it . w) = (( Change_Element_to_Func (F, Borel_Sets ,k)) . w);

      existence

      proof

        deffunc U( Element of Omega) = (( Change_Element_to_Func (F, Borel_Sets ,k)) . $1);

        ex f be Function of Omega, REAL st for d be Element of Omega holds (f . d) = U(d) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of Omega, REAL ;

        assume that

         A1: for w be Element of Omega holds (f1 . w) = (( Change_Element_to_Func (F, Borel_Sets ,k)) . w) and

         A2: for w be Element of Omega holds (f2 . w) = (( Change_Element_to_Func (F, Borel_Sets ,k)) . w);

        let w be Element of Omega;

        (f1 . w) = (( Change_Element_to_Func (F, Borel_Sets ,k)) . w) & (f2 . w) = (( Change_Element_to_Func (F, Borel_Sets ,k)) . w) by A1, A2;

        hence thesis;

      end;

    end

    definition

      let p be Nat;

      let Omega,Omega2 be non empty set;

      let F be SigmaField of Omega;

      let F2 be SigmaField of Omega2;

      let X be set;

      let G be sequence of X;

      :: FINANCE1:def9

      func Element_Of (F,F2,G,p) -> Function of Omega, Omega2 equals

      : Def9: (G . p);

      coherence

      proof

        reconsider p as Element of NAT by ORDINAL1:def 12;

        (G . p) in { f where f be Function of Omega, Omega2 : f is F, F2 -random_variable-like } by A1;

        then ex f be Function of Omega, Omega2 st f = (G . p) & f is F, F2 -random_variable-like;

        hence thesis;

      end;

    end

    definition

      let Omega be non empty set;

      let F be SigmaField of Omega;

      let X be non empty set;

      let w be Element of Omega;

      let G be sequence of X;

      let phi be Real_Sequence;

      :: FINANCE1:def10

      func ElementsOfPortfolioValue_fut (phi,F,w,G) -> Real_Sequence means

      : Def10: for n be Element of NAT holds (it . n) = ((( ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n));

      existence

      proof

        deffunc U( Element of NAT ) = ( In (((( ElementsOfPortfolioValueProb_fut (F,(G . $1))) . w) * (phi . $1)), REAL ));

        consider f be Real_Sequence such that

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

        take f;

        let n be Element of NAT ;

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

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Real_Sequence;

        assume that

         A2: for d be Element of NAT holds (f1 . d) = ((( ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) and

         A3: for d be Element of NAT holds (f2 . d) = ((( ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d));

        let d be Element of NAT ;

        (f1 . d) = ((( ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) & (f2 . d) = ((( ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) by A2, A3;

        hence thesis;

      end;

    end

    definition

      let d be Nat;

      let phi be Real_Sequence;

      let Omega be non empty set;

      let F be SigmaField of Omega;

      let X be non empty set;

      let G be sequence of X;

      let w be Element of Omega;

      :: FINANCE1:def11

      func PortfolioValueFutExt (d,phi,F,G,w) -> Real equals (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . d);

      coherence ;

      :: FINANCE1:def12

      func PortfolioValueFut (d,phi,F,G,w) -> Real equals (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1));

      coherence ;

    end

    registration

      cluster non empty for Element of Borel_Sets ;

      existence

      proof

        consider m be Real such that

         A1: m > -infty ;

        set L = ( halfline m);

        set LL = Family_of_halflines ;

        

         A2: L is non empty by A1, XXREAL_1: 33;

        m in REAL by XREAL_0:def 1;

        then

         A3: L in LL;

         Family_of_halflines is Subset of Borel_Sets by PROB_1:def 9;

        hence thesis by A3, A2;

      end;

    end

    theorem :: FINANCE1:3

    

     Th3: for k be Real holds [.k, +infty .[ is Element of Borel_Sets & ]. -infty , k.[ is Element of Borel_Sets

    proof

      let k be Real;

      

       A1: k in REAL by XREAL_0:def 1;

      set R = ]. -infty , k.[;

      

       A2: ]. -infty , k.[ in Borel_Sets

      proof

        set L = ( halfline k);

        

         A3: L in Family_of_halflines & L = ]. -infty , k.[ by A1;

         Family_of_halflines c= ( sigma Family_of_halflines ) by PROB_1:def 9;

        hence thesis by A3;

      end;

      then (R ` ) in Borel_Sets by PROB_1:def 1;

      hence thesis by Th2, A2;

    end;

    theorem :: FINANCE1:4

    

     Th4: for k1,k2 be Real holds [.k2, k1.[ is Element of Borel_Sets

    proof

      let k1,k2 be Real;

      set R = ]. -infty , k2.[;

      k1 in REAL & k2 in REAL by XREAL_0:def 1;

      then

       A1: -infty < k2 & k1 < +infty by XXREAL_0: 9, XXREAL_0: 12;

      

       A2: ( REAL \ ]. -infty , k2.[) = [.k2, +infty .[ by Th2;

      (R ` ) is Element of Borel_Sets & ]. -infty , k1.[ is Element of Borel_Sets & [.k1, +infty .[ is Element of Borel_Sets by Th3, A2;

      then ( ]. -infty , k1.[ /\ (R ` )) is Element of Borel_Sets by FINSUB_1:def 2;

      then ( ]. -infty , k1.[ /\ [.k2, +infty .[) is Element of Borel_Sets by Th2;

      hence thesis by A1, XXREAL_1: 154;

    end;

    theorem :: FINANCE1:5

    

     Th5: for a,b be Real holds ( Intersection ( half_open_sets (a,b))) is Element of Borel_Sets

    proof

      let a,b be Real;

      for n be Nat holds (( Complement ( half_open_sets (a,b))) . n) is Element of Borel_Sets

      proof

        let n be Nat;

        reconsider nn = n as Element of NAT by ORDINAL1:def 12;

        ((( half_open_sets (a,b)) . nn) ` ) is Element of Borel_Sets

        proof

          (( half_open_sets (a,b)) . n) is Element of Borel_Sets

          proof

            per cases by NAT_1: 6;

              suppose

               A1: n = 0 ;

              (( half_open_sets (a,b)) . 0 ) = ( halfline_fin (a,(b + 1))) by Def1;

              hence thesis by A1, Th4;

            end;

              suppose ex k be Nat st n = (k + 1);

              then

              consider k be Nat such that

               A2: n = (k + 1);

              reconsider k as Element of NAT by ORDINAL1:def 12;

              (( half_open_sets (a,b)) . (k + 1)) = ( halfline_fin (a,(b + (1 / (k + 1))))) by Def1;

              hence thesis by A2, Th4;

            end;

          end;

          hence thesis by PROB_1:def 1;

        end;

        hence thesis by PROB_1:def 2;

      end;

      then ( Complement ( half_open_sets (a,b))) is SetSequence of Borel_Sets by PROB_1: 25;

      then ( Union ( Complement ( half_open_sets (a,b)))) is Element of Borel_Sets by PROB_1: 26;

      hence thesis by PROB_1:def 1;

    end;

    theorem :: FINANCE1:6

    

     Th6: for a,b be Real holds ( Intersection ( half_open_sets (a,b))) = [.a, b.]

    proof

      let a,b be Real;

      

       A1: for c be set holds not c in [.a, b.] implies not c in ( Intersection ( half_open_sets (a,b)))

      proof

        let c be set;

        assume

         A2: not c in [.a, b.];

        per cases by A2;

          suppose not c in REAL ;

          hence thesis;

        end;

          suppose

           A3: c in REAL & not c in [.a, b.];

          then

          reconsider c as Element of REAL ;

          

           A4: not c in { q where q be Element of ExtREAL : a <= q & q <= b } by A3, XXREAL_1:def 1;

          

           A5: a > c or c > b

          proof

            reconsider q = c as Element of ExtREAL by XXREAL_0:def 1;

             not (c = q & a <= c & c <= b) by A4;

            hence thesis;

          end;

          per cases by A5;

            suppose

             A6: a > c;

             not for n be Element of NAT holds c in (( half_open_sets (a,b)) . n)

            proof

              take n = 0 ;

              c in (( half_open_sets (a,b)) . 0 ) implies c in ( halfline_fin (a,(b + 1))) by Def1;

              then c in (( half_open_sets (a,b)) . 0 ) implies c in { q where q be Element of ExtREAL : a <= q & q < (b + 1) } by XXREAL_1:def 2;

              then ex q be Element of ExtREAL st c in (( half_open_sets (a,b)) . 0 ) implies c = q & a <= q & q < (b + 1);

              hence thesis by A6;

            end;

            hence thesis by PROB_1: 13;

          end;

            suppose c > b;

            then

            consider n be Nat such that

             A7: (1 / n) < (c - b) & n > 0 by FRECHET: 36, XREAL_1: 50;

            

             A8: ((1 / n) + b) < ((c - b) + b) by A7, XREAL_1: 6;

            c in ( Intersection ( half_open_sets (a,b))) implies not (b + (1 / n)) < c

            proof

              assume c in ( Intersection ( half_open_sets (a,b)));

              then c in (( half_open_sets (a,b)) . (n + 1)) by PROB_1: 13;

              then c in [.a, (b + (1 / (n + 1))).[ by Def1;

              then c in { q where q be Element of ExtREAL : a <= q & q < (b + (1 / (n + 1))) } by XXREAL_1:def 2;

              then

              consider q be Element of ExtREAL such that

               A9: c = q & a <= q & q < (b + (1 / (n + 1)));

              reconsider a = 1 as Element of NAT ;

              (n * 1) < ((n + 1) * 1) by NAT_1: 13;

              then

               A10: (a / (n + 1)) < (a / n) by A7, XREAL_1: 106;

              (b + (1 / (n + 1))) < (b + (1 / n)) by A10, XREAL_1: 6;

              hence thesis by A9, XXREAL_0: 2;

            end;

            hence thesis by A8;

          end;

        end;

      end;

      

       A11: for c be set holds c in [.a, b.] implies c in ( Intersection ( half_open_sets (a,b)))

      proof

        let c be set;

        c in [.a, b.] implies for n be Nat holds c in (( half_open_sets (a,b)) . n)

        proof

          assume

           A12: c in [.a, b.];

          let n be Nat;

          

           A13: b < (b + 1) by XREAL_1: 29;

           [.a, b.] c= (( half_open_sets (a,b)) . n)

          proof

            per cases ;

              suppose

               A14: n = 0 ;

              (( half_open_sets (a,b)) . 0 ) = ( halfline_fin (a,(b + 1))) by Def1;

              hence thesis by A14, A13, XXREAL_1: 43;

            end;

              suppose n > 0 ;

              then

              consider k be Nat such that

               A15: n = (k + 1) by NAT_1: 6;

              reconsider k as Element of NAT by ORDINAL1:def 12;

              

               A16: (( half_open_sets (a,b)) . (k + 1)) = ( halfline_fin (a,(b + (1 / (k + 1))))) by Def1;

              b < (b + (1 / n)) by A15, XREAL_1: 29;

              hence thesis by A16, A15, XXREAL_1: 43;

            end;

          end;

          hence thesis by A12;

        end;

        hence thesis by PROB_1: 13;

      end;

      for c be object holds c in ( Intersection ( half_open_sets (a,b))) iff c in [.a, b.] by A11, A1;

      hence thesis by TARSKI: 2;

    end;

    theorem :: FINANCE1:7

    for a,b be Real, n be Nat holds (( Partial_Intersection ( half_open_sets (a,b))) . n) is Element of Borel_Sets

    proof

      let a,b be Real;

      defpred J[ Nat] means (( Partial_Intersection ( half_open_sets (a,b))) . $1) is Element of Borel_Sets ;

      

       A1: J[ 0 ]

      proof

        (( Partial_Intersection ( half_open_sets (a,b))) . 0 ) = (( half_open_sets (a,b)) . 0 ) by PROB_3:def 1;

        then (( Partial_Intersection ( half_open_sets (a,b))) . 0 ) = ( halfline_fin (a,(b + 1))) by Def1;

        hence thesis by Th4;

      end;

      

       A2: for k be Nat st J[k] holds J[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: (( Partial_Intersection ( half_open_sets (a,b))) . k) is Element of Borel_Sets ;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        (( Partial_Intersection ( half_open_sets (a,b))) . (k + 1)) = ((( Partial_Intersection ( half_open_sets (a,b))) . k) /\ (( half_open_sets (a,b)) . (k + 1))) by PROB_3:def 1;

        then

         A4: (( Partial_Intersection ( half_open_sets (a,b))) . (k + 1)) = ((( Partial_Intersection ( half_open_sets (a,b))) . k) /\ ( halfline_fin (a,(b + (1 / (k + 1)))))) by Def1;

         [.a, (b + (1 / (k + 1))).[ is Element of Borel_Sets & (( Partial_Intersection ( half_open_sets (a,b))) . k) is Element of Borel_Sets by Th4, A3;

        hence thesis by A4, FINSUB_1:def 2;

      end;

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

      hence thesis;

    end;

    theorem :: FINANCE1:8

    

     Th8: for k1,k2 be Real holds [.k2, k1.] is Element of Borel_Sets

    proof

      let a,b be Real;

      ( Intersection ( half_open_sets (b,a))) = [.b, a.] by Th6;

      hence thesis by Th5;

    end;

    theorem :: FINANCE1:9

    

     Th9: for X be Function of Omega, REAL st X is Sigma, Borel_Sets -random_variable-like holds (for k be Real holds { w where w be Element of Omega : (X . w) >= k } is Element of Sigma & { w where w be Element of Omega : (X . w) < k } is Element of Sigma) & (for k1,k2 be Real st k1 < k2 holds { w where w be Element of Omega : k1 <= (X . w) & (X . w) < k2 } is Element of Sigma) & (for k1,k2 be Real st k1 <= k2 holds { w where w be Element of Omega : k1 <= (X . w) & (X . w) <= k2 } is Element of Sigma) & (for r be Real holds ( less_dom (X,r)) = { w where w be Element of Omega : (X . w) < r }) & (for r be Real holds ( great_eq_dom (X,r)) = { w where w be Element of Omega : (X . w) >= r }) & (for r be Real holds ( eq_dom (X,r)) = { w where w be Element of Omega : (X . w) = r }) & (for r be Real holds ( eq_dom (X,r)) is Element of Sigma)

    proof

      let X be Function of Omega, REAL ;

      assume

       A1: X is Sigma, Borel_Sets -random_variable-like;

      

       A2: for k be Real holds { w where w be Element of Omega : (X . w) >= k } is Element of Sigma & { w where w be Element of Omega : (X . w) < k } is Element of Sigma

      proof

        let k be Real;

        

         A3: for q be set holds (ex w be Element of Omega st q = w & (X . w) >= k) iff (ex w be Element of Omega st q = w & (X . w) in [.k, +infty .])

        proof

          let q be set;

          now

            assume ex w be Element of Omega st q = w & (X . w) in [.k, +infty .];

            then

            consider w be Element of Omega such that

             A4: q = w & (X . w) in [.k, +infty .];

            (X . w) in { z where z be Element of ExtREAL : k <= z & z <= +infty } by A4, XXREAL_1:def 1;

            then ex z be Element of ExtREAL st (X . w) = z & k <= z & z <= +infty ;

            hence ex w be Element of Omega st q = w & (X . w) >= k by A4;

          end;

          hence thesis by XXREAL_1: 219;

        end;

        

         A5: for x be object holds x in { w where w be Element of Omega : (X . w) >= k } iff x in { w where w be Element of Omega : (X . w) in [.k, +infty .[ }

        proof

          let x be object;

          x in { w where w be Element of Omega : (X . w) >= k } iff ex w be Element of Omega st x = w & (X . w) >= k;

          then

           A6: x in { w where w be Element of Omega : (X . w) >= k } iff ex w be Element of Omega st x = w & (X . w) in [.k, +infty .] by A3;

          x in { w where w be Element of Omega : (X . w) in [.k, +infty .] } iff x in { w where w be Element of Omega : (X . w) in [.k, +infty .[ }

          proof

            hereby

              assume x in { w where w be Element of Omega : (X . w) in [.k, +infty .] };

              then

              consider w be Element of Omega such that

               A7: w = x & (X . w) in [.k, +infty .];

              (X . w) in { a where a be Element of ExtREAL : k <= a & a <= +infty } by A7, XXREAL_1:def 1;

              then

              consider a be Element of ExtREAL such that

               A8: (X . w) = a & k <= a & a <= +infty ;

              

               A9: (X . w) = a & k <= a & a < +infty by A8, XXREAL_0: 9;

              { z where z be Element of ExtREAL : k <= z & z < +infty } = [.k, +infty .[ by XXREAL_1:def 2;

              then (X . w) in [.k, +infty .[ by A9;

              hence x in { g where g be Element of Omega : (X . g) in [.k, +infty .[ } by A7;

            end;

            assume x in { w where w be Element of Omega : (X . w) in [.k, +infty .[ };

            then

            consider w be Element of Omega such that

             A10: w = x & (X . w) in [.k, +infty .[;

            w = x & (X . w) in { u where u be Element of ExtREAL : k <= u & u < +infty } by A10, XXREAL_1:def 2;

            then w = x & ex u be Element of ExtREAL st u = (X . w) & k <= u & u < +infty ;

            then w = x & (X . w) in { u where u be Element of ExtREAL : k <= u & u <= +infty };

            then w = x & (X . w) in [.k, +infty .] by XXREAL_1:def 1;

            hence thesis;

          end;

          hence thesis by A6;

        end;

        k in REAL by XREAL_0:def 1;

        then

         A11: [.k, +infty .[ is non empty by XXREAL_0: 9, XXREAL_1: 31;

        

         A12: { w where w be Element of Omega : (X . w) >= k } = { w where w be Element of Omega : (X . w) is Element of [.k, +infty .[ }

        proof

          { w where w be Element of Omega : (X . w) in [.k, +infty .[ } = { w where w be Element of Omega : (X . w) is Element of [.k, +infty .[ }

          proof

            for x be object holds x in { w where w be Element of Omega : (X . w) in [.k, +infty .[ } iff x in { w where w be Element of Omega : (X . w) is Element of [.k, +infty .[ }

            proof

              let x be object;

              hereby

                assume x in { w where w be Element of Omega : (X . w) in [.k, +infty .[ };

                then ex w be Element of Omega st w = x & (X . w) in [.k, +infty .[;

                hence x in { w where w be Element of Omega : (X . w) is Element of [.k, +infty .[ };

              end;

              assume x in { w where w be Element of Omega : (X . w) is Element of [.k, +infty .[ };

              then

              consider w be Element of Omega such that

               A13: w = x & (X . w) is Element of [.k, +infty .[;

              thus thesis by A13, A11;

            end;

            hence thesis by TARSKI: 2;

          end;

          hence thesis by A5, TARSKI: 2;

        end;

        

         A14: [.k, +infty .[ is Element of Borel_Sets & ]. -infty , k.[ is Element of Borel_Sets by Th3;

        

         A15: { w where w be Element of Omega : (X . w) is Element of [.k, +infty .[ } = (X " [.k, +infty .[) by Lm1, A11;

        

         A16: for q be set holds (ex w be Element of Omega st q = w & (X . w) < k) iff (ex w be Element of Omega st q = w & (X . w) in [. -infty , k.[)

        proof

          let q be set;

          now

            assume ex w be Element of Omega st q = w & (X . w) in [. -infty , k.[;

            then

            consider w be Element of Omega such that

             A17: q = w & (X . w) in [. -infty , k.[;

            (X . w) in { z where z be Element of ExtREAL : -infty <= z & z < k } by A17, XXREAL_1:def 2;

            then ex z be Element of ExtREAL st (X . w) = z & -infty <= z & z < k;

            hence ex w be Element of Omega st q = w & (X . w) < k by A17;

          end;

          hence thesis by XXREAL_1: 221;

        end;

        for x be object holds x in { w where w be Element of Omega : (X . w) < k } iff x in { w where w be Element of Omega : (X . w) in ]. -infty , k.[ }

        proof

          let x be object;

          x in { w where w be Element of Omega : (X . w) < k } iff ex w be Element of Omega st x = w & (X . w) < k;

          then

           A18: x in { w where w be Element of Omega : (X . w) < k } iff ex w be Element of Omega st x = w & (X . w) in [. -infty , k.[ by A16;

          x in { w where w be Element of Omega : (X . w) in [. -infty , k.[ } iff x in { w where w be Element of Omega : (X . w) in ]. -infty , k.[ }

          proof

            hereby

              assume x in { w where w be Element of Omega : (X . w) in [. -infty , k.[ };

              then

              consider w be Element of Omega such that

               A19: w = x & (X . w) in [. -infty , k.[;

              (X . w) in { a where a be Element of ExtREAL : -infty <= a & a < k } by A19, XXREAL_1:def 2;

              then

              consider a be Element of ExtREAL such that

               A20: (X . w) = a & -infty <= a & a < k;

              

               A21: (X . w) = a & -infty < a & a < k by A20, XXREAL_0: 12;

              { z where z be Element of ExtREAL : -infty < z & z < k } = ]. -infty , k.[ by XXREAL_1:def 4;

              then (X . w) in ]. -infty , k.[ by A21;

              hence x in { g where g be Element of Omega : (X . g) in ]. -infty , k.[ } by A19;

            end;

            assume x in { w where w be Element of Omega : (X . w) in ]. -infty , k.[ };

            then

            consider w be Element of Omega such that

             A22: w = x & (X . w) in ]. -infty , k.[;

            w = x & (X . w) in { u where u be Element of ExtREAL : -infty < u & u < k } by A22, XXREAL_1:def 4;

            then w = x & ex u be Element of ExtREAL st u = (X . w) & -infty < u & u < k;

            then w = x & (X . w) in { u where u be Element of ExtREAL : -infty <= u & u < k };

            then w = x & (X . w) in [. -infty , k.[ by XXREAL_1:def 2;

            hence thesis;

          end;

          hence thesis by A18;

        end;

        then

         A23: { w where w be Element of Omega : (X . w) < k } = { w where w be Element of Omega : (X . w) in ]. -infty , k.[ } by TARSKI: 2;

        { w where w be Element of Omega : (X . w) < k } is Element of Sigma

        proof

          

           A24: [.k, +infty .[ is Element of Borel_Sets & ]. -infty , k.[ is Element of Borel_Sets by Th3;

          k in REAL by XREAL_0:def 1;

          then

           A25: ]. -infty , k.[ is non empty by XXREAL_0: 12, XXREAL_1: 33;

          then

           A26: { w where w be Element of Omega : (X . w) is Element of ]. -infty , k.[ } = (X " ]. -infty , k.[) by Lm1;

          for x be object holds x in { w where w be Element of Omega : (X . w) in ]. -infty , k.[ } iff x in { w where w be Element of Omega : (X . w) is Element of ]. -infty , k.[ }

          proof

            let x be object;

            hereby

              assume x in { w where w be Element of Omega : (X . w) in ]. -infty , k.[ };

              then ex w be Element of Omega st w = x & (X . w) in ]. -infty , k.[;

              hence x in { w where w be Element of Omega : (X . w) is Element of ]. -infty , k.[ };

            end;

            assume x in { w where w be Element of Omega : (X . w) is Element of ]. -infty , k.[ };

            then

            consider w be Element of Omega such that

             A27: w = x & (X . w) is Element of ]. -infty , k.[;

            thus thesis by A27, A25;

          end;

          

          then { w where w be Element of Omega : (X . w) < k } = { w where w be Element of Omega : (X . w) is Element of ]. -infty , k.[ } by A23, TARSKI: 2

          .= (X " ]. -infty , k.[) by A26;

          hence thesis by A24, A1;

        end;

        hence thesis by A14, A1, A12, A15;

      end;

      

       A28: for k1,k2 be Real st k1 < k2 holds { w where w be Element of Omega : k1 <= (X . w) & (X . w) < k2 } is Element of Sigma

      proof

        let k1,k2 be Real;

        assume

         A29: k1 < k2;

        then

         A30: [.k1, k2.[ is non empty by XXREAL_1: 31;

        { w where w be Element of Omega : k1 <= (X . w) & (X . w) < k2 } is Element of Sigma

        proof

          for x be object holds x in { w where w be Element of Omega : k1 <= (X . w) & (X . w) < k2 } iff x in { w where w be Element of Omega : (X . w) is Element of [.k1, k2.[ }

          proof

            let x be object;

            hereby

              assume x in { w where w be Element of Omega : k1 <= (X . w) & (X . w) < k2 };

              then

              consider w be Element of Omega such that

               A31: x = w & k1 <= (X . w) & (X . w) < k2;

              reconsider a = (X . w) as Element of ExtREAL by XXREAL_0:def 1;

              a = (X . w);

              then (X . w) in { z where z be Element of ExtREAL : k1 <= z & z < k2 } by A31;

              then (X . w) is Element of [.k1, k2.[ by XXREAL_1:def 2;

              hence x in { w1 where w1 be Element of Omega : (X . w1) is Element of [.k1, k2.[ } by A31;

            end;

            assume x in { w where w be Element of Omega : (X . w) is Element of [.k1, k2.[ };

            then

            consider w be Element of Omega such that

             A32: x = w & (X . w) is Element of [.k1, k2.[;

            

             A33: [.k1, k2.[ is non empty by A29, XXREAL_1: 31;

            (X . w) in [.k1, k2.[ by A32, A33;

            then (X . w) in { a where a be Element of ExtREAL : k1 <= a & a < k2 } by XXREAL_1:def 2;

            then ex a be Element of ExtREAL st a = (X . w) & k1 <= a & a < k2;

            hence thesis by A32;

          end;

          then

           A34: { w where w be Element of Omega : k1 <= (X . w) & (X . w) < k2 } = { w where w be Element of Omega : (X . w) is Element of [.k1, k2.[ } by TARSKI: 2;

          

           A35: [.k2, k1.[ is Element of Borel_Sets & [.k1, k2.[ is Element of Borel_Sets by Th4;

          { w where w be Element of Omega : (X . w) is Element of [.k1, k2.[ } = (X " [.k1, k2.[) by Lm1, A30;

          hence thesis by A1, A34, A35;

        end;

        hence thesis;

      end;

      

       A36: for k1,k2 be Real st k1 <= k2 holds { w where w be Element of Omega : k1 <= (X . w) & (X . w) <= k2 } is Element of Sigma

      proof

        let k1,k2 be Real;

        assume

         A37: k1 <= k2;

        then

         A38: [.k1, k2.] is non empty by XXREAL_1: 30;

        for x be object holds (x in { w where w be Element of Omega : k1 <= (X . w) & (X . w) <= k2 } iff x in { w where w be Element of Omega : (X . w) is Element of [.k1, k2.] })

        proof

          let x be object;

          hereby

            assume x in { w where w be Element of Omega : k1 <= (X . w) & (X . w) <= k2 };

            then

            consider w be Element of Omega such that

             A39: x = w & k1 <= (X . w) & (X . w) <= k2;

            reconsider a = (X . w) as Element of ExtREAL by XXREAL_0:def 1;

            a = (X . w);

            then (X . w) in { z where z be Element of ExtREAL : k1 <= z & z <= k2 } by A39;

            then (X . w) is Element of [.k1, k2.] by XXREAL_1:def 1;

            hence x in { w1 where w1 be Element of Omega : (X . w1) is Element of [.k1, k2.] } by A39;

          end;

          assume x in { w where w be Element of Omega : (X . w) is Element of [.k1, k2.] };

          then

          consider w be Element of Omega such that

           A40: x = w & (X . w) is Element of [.k1, k2.];

          

           A41: [.k1, k2.] is non empty by A37, XXREAL_1: 30;

          (X . w) in [.k1, k2.] by A40, A41;

          then (X . w) in { a where a be Element of ExtREAL : k1 <= a & a <= k2 } by XXREAL_1:def 1;

          then ex a be Element of ExtREAL st a = (X . w) & k1 <= a & a <= k2;

          hence thesis by A40;

        end;

        then

         A42: { w where w be Element of Omega : k1 <= (X . w) & (X . w) <= k2 } = { w where w be Element of Omega : (X . w) is Element of [.k1, k2.] } by TARSKI: 2;

        

         A43: [.k1, k2.[ is Element of Borel_Sets & [.k1, k2.] is Element of Borel_Sets by Th8, Th4;

        { w where w be Element of Omega : (X . w) is Element of [.k1, k2.] } = (X " [.k1, k2.]) by Lm1, A38;

        hence thesis by A1, A42, A43;

      end;

      

       A44: for r be Real holds ( less_dom (X,r)) = { w where w be Element of Omega : (X . w) < r }

      proof

        let r be Real;

        for x be object holds x in ( less_dom (X,r)) iff x in { w where w be Element of Omega : (X . w) < r }

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          x in ( less_dom (X,r)) iff x in ( dom X) & (X . xx) < r by MESFUNC1:def 11;

          then x in ( less_dom (X,r)) iff x in Omega & (X . xx) < r by FUNCT_2:def 1;

          then x in ( less_dom (X,r)) iff ex q be Element of Omega st q = x & (X . q) < r;

          hence thesis;

        end;

        hence thesis by TARSKI: 2;

      end;

      

       A45: for r be Real holds ( great_eq_dom (X,r)) = { w where w be Element of Omega : (X . w) >= r }

      proof

        let r be Real;

        for x be object holds x in ( great_eq_dom (X,r)) iff x in { w where w be Element of Omega : (X . w) >= r }

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          x in ( great_eq_dom (X,r)) iff x in ( dom X) & (X . xx) >= r by MESFUNC1:def 14;

          then x in ( great_eq_dom (X,r)) iff x in Omega & (X . xx) >= r by FUNCT_2:def 1;

          then x in ( great_eq_dom (X,r)) iff ex q be Element of Omega st q = x & (X . q) >= r;

          hence thesis;

        end;

        hence thesis by TARSKI: 2;

      end;

      

       A46: for r be Real holds ( eq_dom (X,r)) = { w where w be Element of Omega : (X . w) = r }

      proof

        let r be Real;

        for x be object holds x in ( eq_dom (X,r)) iff x in { w where w be Element of Omega : (X . w) = r }

        proof

          let x be object;

          x in ( eq_dom (X,r)) iff x in ( dom X) & (X . x) = r by MESFUNC1:def 15;

          then x in ( eq_dom (X,r)) iff x in Omega & (X . x) = r by FUNCT_2:def 1;

          then x in ( eq_dom (X,r)) iff (ex q be Element of Omega st q = x & (X . q) = r);

          hence thesis;

        end;

        hence thesis by TARSKI: 2;

      end;

      for r be Real holds ( eq_dom (X,r)) is Element of Sigma

      proof

        let r be Real;

        for x be object holds x in { w where w be Element of Omega : r <= (X . w) & (X . w) <= r } iff x in { w where w be Element of Omega : (X . w) = r }

        proof

          let x be object;

          x in { w where w be Element of Omega : r <= (X . w) & (X . w) <= r } iff ex q be Element of Omega st x = q & r <= (X . q) & (X . q) <= r;

          then x in { w where w be Element of Omega : r <= (X . w) & (X . w) <= r } iff ex q be Element of Omega st x = q & (X . q) = r by XXREAL_0: 1;

          hence thesis;

        end;

        then { w where w be Element of Omega : r <= (X . w) & (X . w) <= r } = { w where w be Element of Omega : (X . w) = r } by TARSKI: 2;

        then { w where w be Element of Omega : (X . w) = r } is Element of Sigma by A36;

        hence thesis by A46;

      end;

      hence thesis by A2, A28, A36, A44, A45, A46;

    end;

    theorem :: FINANCE1:10

    for s be Real, f be Function of Omega, REAL st f = (Omega --> s) holds f is Sigma, Borel_Sets -random_variable-like

    proof

      let s be Real;

      let X be Function of Omega, REAL ;

      assume

       A0: X = (Omega --> s);

      X is Sigma, Borel_Sets -random_variable-like

      proof

        let x be set;

        per cases ;

          suppose

           A1: s in x;

          for q be object holds q in { w where w be Element of Omega : (X . w) is Element of x } iff q in Omega

          proof

            let q be object;

            hereby

              assume q in { w where w be Element of Omega : (X . w) is Element of x };

              then ex w be Element of Omega st w = q & (X . w) is Element of x;

              hence q in Omega;

            end;

            assume q in Omega;

            then

            reconsider w = q as Element of Omega;

            (X . w) is Element of x by A1, FUNCOP_1: 7, A0;

            hence thesis;

          end;

          then

           A2: { w where w be Element of Omega : (X . w) is Element of x } = Omega by TARSKI: 2;

          x is non empty by A1;

          then { w where w be Element of Omega : (X . w) is Element of x } = (X " x) by Lm1;

          then (X " x) = Omega by A2;

          then (X " x) is Element of Sigma by PROB_1: 23;

          hence thesis;

        end;

          suppose

           A3: not s in x;

          for q be object holds q in (X " x) iff q in {}

          proof

            let q be object;

            now

              assume q in (X " x);

              then q in ( dom X) & (X . q) in x by FUNCT_1:def 7;

              hence q in {} by A3, FUNCOP_1: 7, A0;

            end;

            hence thesis;

          end;

          then (X " x) = {} by TARSKI: 2;

          then (X " x) is Element of Sigma by PROB_1: 22;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FINANCE1:11

    

     Th11: for phi be Real_Sequence, jpi be pricefunction, d be Nat st d > 0 holds ( BuyPortfolioExt (phi,jpi,d)) = ((phi . 0 ) + ( BuyPortfolio (phi,jpi,d)))

    proof

      let phi be Real_Sequence, jpi be pricefunction, d be Nat;

      assume d > 0 ;

      then

       A1: (d - 1) is Element of NAT by NAT_1: 20;

      defpred J[ Nat] means (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ($1 + 1)) = ((phi . 0 ) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . $1));

      (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ( 0 + 1)) = ((phi . 0 ) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0 ))

      proof

        (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ( 0 + 1)) = ((( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . 0 ) + (( ElementsOfBuyPortfolio (phi,jpi)) . 1)) by SERIES_1:def 1;

        then (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ( 0 + 1)) = ((( ElementsOfBuyPortfolio (phi,jpi)) . 0 ) + (( ElementsOfBuyPortfolio (phi,jpi)) . 1)) by SERIES_1:def 1;

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

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

        then (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ( 0 + 1)) = (((phi . 0 ) * (jpi . 0 )) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0 )) by VALUED_1: 5;

        then (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ( 0 + 1)) = (((phi . 0 ) * 1) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0 )) by Def2;

        hence thesis;

      end;

      then

       A2: J[ 0 ];

      

       A3: for k be Nat st J[k] holds J[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . (k + 1)) = ((phi . 0 ) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k));

        reconsider k as Element of NAT by ORDINAL1:def 12;

        (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1)) = (((phi . 0 ) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k)) + (( ElementsOfBuyPortfolio (phi,jpi)) . ((k + 1) + 1))) by A4, SERIES_1:def 1;

        then (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1)) = (((phi . 0 ) + (( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k)) + ((( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (k + 1))) by NAT_1:def 3;

        then (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1)) = ((phi . 0 ) + ((( Partial_Sums (( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) + ((( ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (k + 1))));

        hence thesis by SERIES_1:def 1;

      end;

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

      then (( Partial_Sums ( ElementsOfBuyPortfolio (phi,jpi))) . ((d - 1) + 1)) = ((phi . 0 ) + ( BuyPortfolio (phi,jpi,d))) by A1;

      hence thesis;

    end;

    theorem :: FINANCE1:12

    

     Th12: for d be Nat st d > 0 holds for r be Real holds for phi be Real_Sequence 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 for w be Element of Omega holds ( PortfolioValueFutExt (d,phi,F,G,w)) = (((1 + r) * (phi . 0 )) + ( PortfolioValueFut (d,phi,F,G,w)))

    proof

      let d be Nat;

      assume

       A1: d > 0 ;

      let r be Real;

      let phi be Real_Sequence;

      set X = ( set_of_random_variables_on (F, Borel_Sets ));

      let G be sequence of X;

      assume

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

      let w be Element of Omega;

      

       A3: (d - 1) is Element of NAT by A1, NAT_1: 20;

      defpred J[ Nat] means (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ($1 + 1)) = (((1 + r) * (phi . 0 )) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . $1));

      (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ( 0 + 1)) = (((1 + r) * (phi . 0 )) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0 ))

      proof

        (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ( 0 + 1)) = ((( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0 ) + (( ElementsOfPortfolioValue_fut (phi,F,w,G)) . 1)) by SERIES_1:def 1;

        then (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ( 0 + 1)) = ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0 ) + (( ElementsOfPortfolioValue_fut (phi,F,w,G)) . 1)) by SERIES_1:def 1;

        then (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ( 0 + 1)) = ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0 ) + ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . 0 )) by NAT_1:def 3;

        then (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ( 0 + 1)) = ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0 ) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0 )) by SERIES_1:def 1;

        then

        consider d be Element of NAT such that

         A4: d = 0 & (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . (d + 1)) = ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) . d) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . d));

        

         A5: (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . (d + 1)) = (((( ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . d)) by A4, Def10;

        set g = (G . d);

        set g2 = ( Change_Element_to_Func (F, Borel_Sets ,g));

        (g2 . w) = (1 + r)

        proof

          ( Element_Of (F, Borel_Sets ,G, 0 )) = (G . 0 ) & g2 = (G . 0 ) & ( Element_Of (F, Borel_Sets ,G, 0 )) = (Omega --> (1 + r)) by A2, Def9, Def7, A4;

          hence thesis by FUNCOP_1: 7;

        end;

        hence thesis by A4, A5, Def8;

      end;

      then

       A6: J[ 0 ];

      

       A7: for k be Nat st J[k] holds J[(k + 1)]

      proof

        let k be Nat;

        assume

         A8: (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . (k + 1)) = (((1 + r) * (phi . 0 )) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k));

        reconsider k as Element of NAT by ORDINAL1:def 12;

        (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1)) = ((((1 + r) * (phi . 0 )) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)) + (( ElementsOfPortfolioValue_fut (phi,F,w,G)) . ((k + 1) + 1))) by A8, SERIES_1:def 1;

        then (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1)) = ((((1 + r) * (phi . 0 )) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)) + ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (k + 1))) by NAT_1:def 3;

        then (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1)) = (((1 + r) * (phi . 0 )) + ((( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k) + ((( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (k + 1))));

        hence thesis by SERIES_1:def 1;

      end;

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

      then (( Partial_Sums ( ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((d - 1) + 1)) = (((1 + r) * (phi . 0 )) + (( Partial_Sums (( ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1))) by A3;

      hence thesis;

    end;

    theorem :: FINANCE1:13

    

     Th13: for d be Nat st d > 0 holds for r be Real st r > ( - 1) holds for phi be Real_Sequence, jpi be pricefunction 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 for w be Element of Omega holds ( BuyPortfolioExt (phi,jpi,d)) <= 0 implies (( PortfolioValueFutExt (d,phi,F,G,w)) <= (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolio (phi,jpi,d)))))

    proof

      let d be Nat;

      assume

       A1: d > 0 ;

      let r be Real;

      assume

       A2: r > ( - 1);

      let phi be Real_Sequence, jpi be pricefunction;

      set X = ( set_of_random_variables_on (F, Borel_Sets ));

      let G be sequence of X;

      assume

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

      let w be Element of Omega;

      assume

       A4: ( BuyPortfolioExt (phi,jpi,d)) <= 0 ;

      

       A5: ((1 + r) * ( BuyPortfolioExt (phi,jpi,d))) <= 0

      proof

        (1 + r) > 0 by A2, XREAL_1: 62;

        hence thesis by A4;

      end;

      (((1 + r) * ( BuyPortfolioExt (phi,jpi,d))) + (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolioExt (phi,jpi,d))))) <= (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolioExt (phi,jpi,d)))) by A5, XREAL_1: 32;

      then ( PortfolioValueFut (d,phi,F,G,w)) <= (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ((phi . 0 ) + ( BuyPortfolio (phi,jpi,d))))) by A1, Th11;

      then ( PortfolioValueFut (d,phi,F,G,w)) <= ((( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) - ((1 + r) * (phi . 0 )));

      then (( PortfolioValueFut (d,phi,F,G,w)) + ((1 + r) * (phi . 0 ))) <= (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) by XREAL_1: 19;

      hence thesis by A1, A3, Th12;

    end;

    theorem :: FINANCE1:14

    for d be Nat st d > 0 holds for r be Real st r > ( - 1) holds for phi be Real_Sequence, jpi be pricefunction 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 (( BuyPortfolioExt (phi,jpi,d)) <= 0 implies ({ w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) >= 0 } c= { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) >= ((1 + r) * ( BuyPortfolio (phi,jpi,d))) } & { w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) > 0 } c= { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) > ((1 + r) * ( BuyPortfolio (phi,jpi,d))) }))

    proof

      let d be Nat;

      assume

       A1: d > 0 ;

      let r be Real;

      assume

       A2: r > ( - 1);

      let phi be Real_Sequence, jpi be pricefunction;

      set X = ( set_of_random_variables_on (F, Borel_Sets ));

      let G be sequence of X;

      assume

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

      assume

       A4: ( BuyPortfolioExt (phi,jpi,d)) <= 0 ;

      

       A5: { w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) >= 0 } c= { w where w be Element of Omega : ( PortfolioValueFut (d,phi,F,G,w)) >= ((1 + r) * ( BuyPortfolio (phi,jpi,d))) }

      proof

        let x be object;

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

        then

        consider w be Element of Omega such that

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

         0 <= (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) by A1, A2, A3, A4, Th13, A6;

        then ( 0 + ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) <= ( PortfolioValueFut (d,phi,F,G,w)) by XREAL_1: 19;

        hence thesis by A6;

      end;

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

      proof

        let x be object;

        assume x in { w where w be Element of Omega : ( PortfolioValueFutExt (d,phi,F,G,w)) > 0 };

        then

        consider w be Element of Omega such that

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

        ( PortfolioValueFutExt (d,phi,F,G,w)) <= (( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) by A1, A2, A3, A4, Th13;

        then ( 0 + ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) < ((( PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) + ((1 + r) * ( BuyPortfolio (phi,jpi,d)))) by A7, XREAL_1: 6;

        hence thesis by A7;

      end;

      hence thesis by A5;

    end;

    theorem :: FINANCE1:15

    

     Th15: for f be Function of Omega, REAL st f is Sigma, Borel_Sets -random_variable-like holds f is ( [#] Sigma) -measurable & f is Real-Valued-Random-Variable of Sigma

    proof

      let f be Function of Omega, REAL ;

      assume

       A1: f is Sigma, Borel_Sets -random_variable-like;

      

       A2: for r be Element of REAL holds (Omega /\ ( less_dom (f,r))) in Sigma

      proof

        let r be Element of REAL ;

        ( less_dom (f,r)) = { w where w be Element of Omega : (f . w) < r } by A1, Th9;

        then ( less_dom (f,r)) is Element of Sigma by A1, Th9;

        then ( less_dom (f,r)) in Sigma;

        hence thesis by XBOOLE_1: 28;

      end;

      

       A3: for r be Real holds (( [#] Sigma) /\ ( less_dom (f,r))) in Sigma

      proof

        let r be Real;

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

        (( [#] Sigma) /\ ( less_dom (f,r))) in Sigma by A2;

        hence thesis;

      end;

      then f is ( [#] Sigma) -measurable by MESFUNC6: 12;

      then f is Real-Valued-Random-Variable of Sigma by RANDOM_1:def 2;

      hence thesis by A3, MESFUNC6: 12;

    end;

    theorem :: FINANCE1:16

    ( set_of_random_variables_on (Sigma, Borel_Sets )) c= ( Real-Valued-Random-Variables-Set Sigma)

    proof

      let x be object;

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

      then

      consider f be Function of Omega, REAL such that

       A1: x = f & f is Sigma, Borel_Sets -random_variable-like;

      

       A2: f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma by Th15;

      x in the set of all q where q be Real-Valued-Random-Variable of Sigma by A2, A1;

      hence thesis by RANDOM_2:def 3;

    end;

    theorem :: FINANCE1:17

    (Omega --> the Element of Omega2) is random_variable of F, F2 by LemmaExample;