random_3.miz



    begin

    reserve Omega,Omega1,Omega2 for non empty set;

    reserve Sigma for SigmaField of Omega;

    reserve S1 for SigmaField of Omega1;

    reserve S2 for SigmaField of Omega2;

    theorem :: RANDOM_3:1

    

     Th1: for B be non empty set, f be Function holds (f " ( union B)) = ( union the set of all (f " Y) where Y be Element of B)

    proof

      let B be non empty set, f be Function;

      set Z = the set of all (f " Y) where Y be Element of B;

      thus (f " ( union B)) c= ( union Z)

      proof

        let x be object;

        assume

         A1: x in (f " ( union B));

        then (f . x) in ( union B) by FUNCT_1:def 7;

        then

        consider Y be set such that

         A2: (f . x) in Y and

         A3: Y in B by TARSKI:def 4;

        reconsider Y as Element of B by A3;

        x in ( dom f) by A1, FUNCT_1:def 7;

        then

         A4: x in (f " Y) by A2, FUNCT_1:def 7;

        (f " Y) in Z;

        hence x in ( union Z) by A4, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union Z);

      then

      consider Y be set such that

       A5: x in Y and

       A6: Y in Z by TARSKI:def 4;

      consider D be Element of B such that

       A7: Y = (f " D) by A6;

      (f " D) c= (f " ( union B)) by RELAT_1: 143, ZFMISC_1: 74;

      hence x in (f " ( union B)) by A5, A7;

    end;

    theorem :: RANDOM_3:2

    

     Th2: for f be Function of Omega1, Omega2, B be SetSequence of Omega2, D be SetSequence of Omega1 st for n be Element of NAT holds (D . n) = (f " (B . n)) holds (f " ( Union B)) = ( Union D)

    proof

      let f be Function of Omega1, Omega2, B be SetSequence of Omega2, D be SetSequence of Omega1;

      assume

       A1: for n be Element of NAT holds (D . n) = (f " (B . n));

      set Z = ( rng D);

      set Q = the set of all (f " Y) where Y be Element of ( rng B);

      for x be object holds x in Z iff x in Q

      proof

        let x be object;

        hereby

          assume x in Z;

          then

          consider n be Element of NAT such that

           A2: x = (D . n) by FUNCT_2: 113;

          

           A3: x = (f " (B . n)) by A1, A2;

          (B . n) in ( rng B) by FUNCT_2: 112;

          hence x in Q by A3;

        end;

        assume x in Q;

        then

        consider Y be Element of ( rng B) such that

         A4: x = (f " Y);

        consider n be Element of NAT such that

         A5: Y = (B . n) by FUNCT_2: 113;

        x = (D . n) by A1, A4, A5;

        hence x in Z by FUNCT_2: 112;

      end;

      then Z = Q by TARSKI: 2;

      hence thesis by Th1;

    end;

    theorem :: RANDOM_3:3

    

     Th3: for f be Function of Omega1, Omega2, B be SetSequence of Omega2, D be SetSequence of Omega1 st for n be Element of NAT holds (D . n) = (f " (B . n)) holds (f " ( Intersection B)) = ( Intersection D)

    proof

      let f be Function of Omega1, Omega2, B be SetSequence of Omega2, D be SetSequence of Omega1;

      assume

       A1: for n be Element of NAT holds (D . n) = (f " (B . n));

      set Z = the set of all (f " (B . n)) where n be Element of NAT ;

      set Q = the set of all (f " Y) where Y be Element of ( rng B);

      set E = ( Complement D);

      

       A2: for n be Element of NAT holds (E . n) = (f " (( Complement B) . n))

      proof

        let n be Element of NAT ;

        

        thus (E . n) = ((D . n) ` ) by PROB_1:def 2

        .= ((f " (B . n)) ` ) by A1

        .= ((f " Omega2) \ (f " (B . n))) by FUNCT_2: 40

        .= (f " ((B . n) ` )) by FUNCT_1: 69

        .= (f " (( Complement B) . n)) by PROB_1:def 2;

      end;

      (f " ( Intersection B)) = ((f " Omega2) \ (f " ( union ( rng ( Complement B))))) by FUNCT_1: 69

      .= (Omega1 \ (f " ( Union ( Complement B)))) by FUNCT_2: 40

      .= (Omega1 \ ( Union E)) by Th2, A2

      .= (Omega1 \ ( union ( rng E)));

      hence thesis;

    end;

    theorem :: RANDOM_3:4

    

     Th4: for F be Function of Omega, REAL , r be Real st F is Real-Valued-Random-Variable of Sigma holds (F " ]. -infty , r.[) in Sigma

    proof

      let F be Function of Omega, REAL ;

      let r be Real;

      assume F is Real-Valued-Random-Variable of Sigma;

      then F is ( [#] Sigma) -measurable by RANDOM_1:def 2;

      then

       A2: (( [#] Sigma) /\ ( less_dom (F,r))) in Sigma by MESFUNC6: 12;

      for z be object holds z in (F " ]. -infty , r.[) iff z in (( [#] Sigma) /\ ( less_dom (F,r)))

      proof

        let z be object;

        hereby

          assume

           A3: z in (F " ]. -infty , r.[);

          then

           A4: z in ( dom F) & (F . z) in ]. -infty , r.[ by FUNCT_1:def 7;

          then (F . z) in { p where p be Real : -infty < p & p < r } by RCOMP_1:def 2;

          then

          consider w be Real such that

           A5: (F . z) = w & -infty < w & w < r;

          z in ( less_dom (F,r)) by A4, A5, MESFUNC1:def 11;

          hence z in (( [#] Sigma) /\ ( less_dom (F,r))) by A3, XBOOLE_0:def 4;

        end;

        assume z in (( [#] Sigma) /\ ( less_dom (F,r)));

        then

         A6: z in ( [#] Sigma) & z in ( less_dom (F,r)) by XBOOLE_0:def 4;

        then

         A7: z in ( dom F) & (F . z) < r by MESFUNC1:def 11;

         -infty < (F . z) & (F . z) < r by XXREAL_0: 12, FUNCT_2: 5, MESFUNC1:def 11, A6;

        then (F . z) in { p where p be Real : -infty < p & p < r };

        then (F . z) in ]. -infty , r.[ by RCOMP_1:def 2;

        hence z in (F " ]. -infty , r.[) by A7, FUNCT_1:def 7;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: RANDOM_3:5

    

     Th5: for F be Function of Omega, REAL st F is Real-Valued-Random-Variable of Sigma holds { x where x be Element of Borel_Sets : (F " x) is Element of Sigma } is SigmaField of REAL

    proof

      let F be Function of Omega, REAL ;

      assume

       A1: F is Real-Valued-Random-Variable of Sigma;

      set S = { x where x be Element of Borel_Sets : (F " x) is Element of Sigma };

      for x be object st x in S holds x in Borel_Sets

      proof

        let z be object;

        assume z in S;

        then ex x be Element of Borel_Sets st x = z & (F " x) is Element of Sigma;

        hence z in Borel_Sets ;

      end;

      then

       A2: S c= Borel_Sets ;

      set r0 = the Element of REAL ;

      

       A3: ( halfline r0) in Family_of_halflines ;

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

      then

      reconsider y0 = ( halfline r0) as Element of Borel_Sets by A3;

      (F " y0) is Element of Sigma by Th4, A1;

      then

       A4: y0 in S;

      

       A5: for A be Subset of REAL st A in S holds (A ` ) in S

      proof

        let A be Subset of REAL ;

        assume A in S;

        then

        consider x be Element of Borel_Sets such that

         A6: A = x & (F " x) is Element of Sigma;

        

         A7: (F " ( REAL \ x)) = ((F " REAL ) \ (F " x)) by FUNCT_1: 69

        .= (Omega \ (F " x)) by FUNCT_2: 40;

         REAL is Element of Borel_Sets by PROB_1: 5;

        then

         A8: ( REAL \ x) is Element of Borel_Sets by PROB_1: 6;

        Omega is Element of Sigma by PROB_1: 5;

        then (Omega \ (F " x)) is Element of Sigma by A6, PROB_1: 6;

        hence (A ` ) in S by A6, A7, A8;

      end;

      for A1 be SetSequence of REAL st ( rng A1) c= S holds ( Intersection A1) in S

      proof

        let A1 be SetSequence of REAL ;

        assume

         A9: ( rng A1) c= S;

        then

         A10: ( rng A1) c= Borel_Sets by A2;

        then

         A11: ( Intersection A1) in Borel_Sets by PROB_1: 15;

        reconsider B1 = ( Intersection A1) as Element of Borel_Sets by PROB_1: 15, A10;

        deffunc G( set) = (F " (A1 . $1));

        

         A12: for n be Element of NAT holds G(n) is Element of Sigma

        proof

          let n be Element of NAT ;

          (A1 . n) in ( rng A1) by FUNCT_2: 112;

          then (A1 . n) in S by A9;

          then ex x be Element of Borel_Sets st x = (A1 . n) & (F " x) is Element of Sigma;

          hence G(n) is Element of Sigma;

        end;

        consider D be Function of NAT , Sigma such that

         A13: for n be Element of NAT holds (D . n) = G(n) from FUNCT_2:sch 9( A12);

        D in ( Funcs ( NAT ,Sigma)) by FUNCT_2: 8;

        then

         A14: ex f be Function st D = f & ( dom f) = NAT & ( rng f) c= Sigma by FUNCT_2:def 2;

        ( rng D) c= ( bool Omega);

        then

        reconsider D as SetSequence of Omega by FUNCT_2: 6;

        

         A15: ( Intersection D) in Sigma by A14, PROB_1: 15;

        (F " ( Intersection A1)) = ( Intersection D) by A13, Th3;

        hence ( Intersection A1) in S by A11, A15;

      end;

      hence S is SigmaField of REAL by PROB_1: 15, A4, A5, XBOOLE_1: 1, A2;

    end;

    theorem :: RANDOM_3:6

    

     Th6: for f be Function of Omega, REAL st f is Real-Valued-Random-Variable of Sigma holds { x where x be Element of Borel_Sets : (f " x) is Element of Sigma } = Borel_Sets

    proof

      let f be Function of Omega, REAL ;

      assume

       A1: f is Real-Valued-Random-Variable of Sigma;

      set B = { x where x be Element of Borel_Sets : (f " x) is Element of Sigma };

      now

        let z be object;

        assume

         A2: z in Family_of_halflines ;

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

        then

        reconsider y = z as Element of Borel_Sets by A2;

        consider r be Element of REAL such that

         A3: y = ( halfline r) by A2;

        (f " y) is Element of Sigma by A1, Th4, A3;

        hence z in B;

      end;

      then

       A4: Family_of_halflines c= B;

      B is SigmaField of REAL by Th5, A1;

      then

       A5: Borel_Sets c= B by A4, PROB_1:def 9;

      now

        let x be object;

        assume x in B;

        then ex z be Element of Borel_Sets st z = x & (f " z) is Element of Sigma;

        hence x in Borel_Sets ;

      end;

      then B c= Borel_Sets ;

      hence B = Borel_Sets by A5;

    end;

    theorem :: RANDOM_3:7

    

     Th7: for f be Function of Omega, REAL holds f is Sigma, Borel_Sets -random_variable-like iff f is Real-Valued-Random-Variable of Sigma

    proof

      let f be Function of Omega, REAL ;

      thus f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma by FINANCE1: 15;

      assume

       A1: f is Real-Valued-Random-Variable of Sigma;

      set B = { x where x be Element of Borel_Sets : (f " x) is Element of Sigma };

      

       A2: B = Borel_Sets by Th6, A1;

      for x be set st x in Borel_Sets holds (f " x) in Sigma

      proof

        let x be set;

        assume x in Borel_Sets ;

        then ex z be Element of Borel_Sets st z = x & (f " z) is Element of Sigma by A2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RANDOM_3:8

    for f be Function of Omega, REAL holds ( set_of_random_variables_on (Sigma, Borel_Sets )) = ( Real-Valued-Random-Variables-Set Sigma)

    proof

      let f be Function of Omega, REAL ;

      for x be object holds x in ( set_of_random_variables_on (Sigma, Borel_Sets )) iff x in ( Real-Valued-Random-Variables-Set Sigma)

      proof

        let x be object;

        hereby

          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;

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

          hence x in ( Real-Valued-Random-Variables-Set Sigma) by A1;

        end;

        assume x in ( Real-Valued-Random-Variables-Set Sigma);

        then

        consider q be Real-Valued-Random-Variable of Sigma such that

         A2: x = q;

        q is Sigma, Borel_Sets -random_variable-like by Th7;

        hence x in ( set_of_random_variables_on (Sigma, Borel_Sets )) by A2;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      ::$Canceled

    end

    registration

      let Omega1, Omega2, S1, S2;

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

      existence

      proof

        set F = the Element of ( set_of_random_variables_on (S1,S2));

        F in ( set_of_random_variables_on (S1,S2));

        then ex f be Function of Omega1, Omega2 st F = f & f is S1, S2 -random_variable-like;

        hence thesis;

      end;

    end

    definition

      let Omega1, Omega2, S1, S2;

      mode random_variable of S1,S2 is S1, S2 -random_variable-like Function of Omega1, Omega2;

    end

    theorem :: RANDOM_3:9

    for f be Function of Omega, REAL holds f is random_variable of Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma by Th7;

    definition

      let F be Function;

      :: RANDOM_3:def2

      attr F is random_variable_family-like means

      : Def2: for x be set st x in ( dom F) holds ex Omega1,Omega2 be non empty set, S1 be SigmaField of Omega1, S2 be SigmaField of Omega2, f be random_variable of S1, S2 st (F . x) = f;

    end

    registration

      cluster random_variable_family-like for Function;

      existence

      proof

        set Omega1 = the non empty set;

        set S1 = the SigmaField of Omega1;

        set M = the random_variable of S1, S1;

        set F = ( {1} --> M);

        for x be set st x in ( dom F) holds ex Omega1,Omega2 be non empty set, S1 be SigmaField of Omega1, S2 be SigmaField of Omega2, f be random_variable of S1, S2 st (F . x) = f by FUNCOP_1: 7;

        hence thesis by Def2;

      end;

    end

    definition

      mode random_variable_family is random_variable_family-like Function;

    end

    reserve F for random_variable of S1, S2;

    definition

      let Y be non empty set;

      let S be SigmaField of Y;

      let F be Function;

      :: RANDOM_3:def3

      attr F is S -Measure_valued means

      : Def3: for x be set st x in ( dom F) holds ex M be sigma_Measure of S st (F . x) = M;

    end

    registration

      let Y be non empty set;

      let S be SigmaField of Y;

      cluster S -Measure_valued for Function;

      existence

      proof

        set M = the sigma_Measure of S;

        set F = ( {1} --> M);

        for x be set st x in ( dom F) holds ex MM be sigma_Measure of S st (F . x) = MM by FUNCOP_1: 7;

        hence thesis by Def3;

      end;

    end

    definition

      let Y be non empty set;

      let S be SigmaField of Y;

      let F be Function;

      :: RANDOM_3:def4

      attr F is S -Probability_valued means

      : Def4: for x be set st x in ( dom F) holds ex P be Probability of S st (F . x) = P;

    end

    registration

      let Y be non empty set;

      let S be SigmaField of Y;

      cluster S -Probability_valued for Function;

      existence

      proof

        set M = the Probability of S;

        set F = ( {1} --> M);

        for x be set st x in ( dom F) holds ex P be Probability of S st (F . x) = P by FUNCOP_1: 7;

        hence thesis by Def4;

      end;

    end

    

     Lm1: for X,Y be non empty set, S be SigmaField of Y, M be Probability of S holds (X --> M) is S -Probability_valued by FUNCOP_1: 7;

    registration

      let X,Y be non empty set;

      let S be SigmaField of Y;

      cluster X -defined for S -Probability_valued Function;

      existence

      proof

        (X --> the Probability of S) is S -Probability_valued Function by Lm1;

        hence thesis;

      end;

    end

    registration

      let X,Y be non empty set;

      let S be SigmaField of Y;

      cluster total for X -definedS -Probability_valued Function;

      existence

      proof

        (X --> the Probability of S) is S -Probability_valued Function by Lm1;

        hence thesis;

      end;

    end

    registration

      let Y be non empty set, S be SigmaField of Y;

      cluster S -Probability_valued -> S -Measure_valued for Function;

      coherence

      proof

        let F be Function;

        assume

         A1: F is S -Probability_valued;

        let y be set;

        assume y in ( dom F);

        then

        consider P be Probability of S such that

         A2: (F . y) = P by A1;

        take ( P2M P);

        thus thesis by A2;

      end;

    end

    definition

      let Y be non empty set;

      let S be SigmaField of Y;

      let F be Function;

      :: RANDOM_3:def5

      attr F is S -Random-Variable-Family means

      : Def5: for x be set st x in ( dom F) holds ex Z be Real-Valued-Random-Variable of S st (F . x) = Z;

    end

    registration

      let Y be non empty set;

      let S be SigmaField of Y;

      cluster S -Random-Variable-Family for Function;

      existence

      proof

        set M = the Real-Valued-Random-Variable of S;

        set F = ( {1} --> M);

        for x be set st x in ( dom F) holds ex Z be Real-Valued-Random-Variable of S st (F . x) = Z by FUNCOP_1: 7;

        hence thesis by Def5;

      end;

    end

    theorem :: RANDOM_3:10

    for y be Element of S2 st y <> {} holds { z where z be Element of Omega1 : (F . z) is Element of y } = (F " y)

    proof

      let y be Element of S2;

      assume

       A1: y <> {} ;

      set D = { z where z be Element of Omega1 : (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 Omega1 such that

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

          z in Omega1;

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

          hence x in (F " y) by A2, FUNCT_1:def 7, A1;

        end;

        assume x in (F " y);

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

        hence x in D;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RANDOM_3:11

    for F be random_variable of S1, S2 holds { x where x be Subset of Omega1 : ex y be Element of S2 st x = (F " y) } c= S1 & { x where x be Subset of Omega1 : ex y be Element of S2 st x = (F " y) } is SigmaField of Omega1

    proof

      let F be random_variable of S1, S2;

      set S = { x where x be Subset of Omega1 : ex y be Element of S2 st x = (F " y) };

      for x be object st x in S holds x in S1

      proof

        let z be object;

        assume z in S;

        then

        consider x be Subset of Omega1 such that

         A1: z = x & ex y be Element of S2 st x = (F " y);

        thus z in S1 by A1, FINANCE1:def 5;

      end;

      hence

       A2: S c= S1;

       {} is Element of S2 by PROB_1: 22;

      then

       A3: (F " {} ) in S;

      

       A4: for A be Subset of Omega1 st A in S holds (A ` ) in S

      proof

        let A be Subset of Omega1;

        assume A in S;

        then

        consider x be Subset of Omega1 such that

         A5: A = x & ex y be Element of S2 st x = (F " y);

        consider y be Element of S2 such that

         A6: x = (F " y) by A5;

        

         A7: (y ` ) in S2 by PROB_1:def 1;

        (F " (y ` )) = ((F " Omega2) \ (F " y)) by FUNCT_1: 69

        .= (A ` ) by A5, A6, FUNCT_2: 40;

        hence (A ` ) in S by A7;

      end;

      for A1 be SetSequence of Omega1 st ( rng A1) c= S holds ( Intersection A1) in S

      proof

        let A1 be SetSequence of Omega1;

        assume

         A8: ( rng A1) c= S;

        defpred Q[ set, set] means (A1 . $1) = (F " $2) & $2 in S2;

        

         A9: for n be Element of NAT holds ex Bn be Element of ( bool Omega2) st Q[n, Bn]

        proof

          let n be Element of NAT ;

          (A1 . n) in ( rng A1) by FUNCT_2: 112;

          then (A1 . n) in S by A8;

          then

          consider x be Subset of Omega1 such that

           A10: (A1 . n) = x & ex y be Element of S2 st x = (F " y);

          thus thesis by A10;

        end;

        consider B be Function of NAT , ( bool Omega2) such that

         A11: for x be Element of NAT holds Q[x, (B . x)] from FUNCT_2:sch 3( A9);

        reconsider B as SetSequence of ( bool Omega2);

        now

          let y be object;

          assume y in ( rng B);

          then

          consider x be object such that

           A12: x in NAT & (B . x) = y by FUNCT_2: 11;

          reconsider x as Element of NAT by A12;

          thus y in S2 by A12, A11;

        end;

        then ( rng B) c= S2;

        then

        reconsider B1 = ( Intersection B) as Element of S2 by PROB_1: 15;

        (F " B1) = ( Intersection A1) by Th3, A11;

        hence ( Intersection A1) in S;

      end;

      hence S is SigmaField of Omega1 by PROB_1: 15, A3, A4, A2, XBOOLE_1: 1;

    end;

    

     Lm2: for M be Measure of S1, F be random_variable of S1, S2 holds ex N be Measure of S2 st for y be Element of S2 holds (N . y) = (M . (F " y))

    proof

      let M be Measure of S1, F be random_variable of S1, S2;

      deffunc G( set) = (M . (F " $1));

      

       A1: for y be set st y in S2 holds G(y) in ExtREAL ;

      consider N be Function of S2, ExtREAL such that

       A2: for y be set st y in S2 holds (N . y) = G(y) from FUNCT_2:sch 11( A1);

      

       A3: for y be Element of S2 holds (N . y) = G(y) by A2;

      now

        let A be Element of S2;

        (F " A) in S1 by FINANCE1:def 5;

        then 0. <= (M . (F " A)) by MEASURE1:def 2;

        hence 0. <= (N . A) by A2;

      end;

      then

       A4: N is nonnegative by MEASURE1:def 2;

      now

        let A,B be Element of S2;

        assume

         A5: A misses B;

        

         A6: ((F " A) /\ (F " B)) = (F " (A /\ B)) by FUNCT_1: 68

        .= (F " {} ) by A5

        .= {} ;

        

         A7: (F " A) in S1 by FINANCE1:def 5;

        

         A8: (F " B) in S1 by FINANCE1:def 5;

        

        thus (N . (A \/ B)) = (M . (F " (A \/ B))) by A2

        .= (M . ((F " A) \/ (F " B))) by RELAT_1: 140

        .= ((M . (F " A)) + (M . (F " B))) by A6, A7, A8, MEASURE1:def 8, XBOOLE_0:def 7

        .= ((N . A) + (M . (F " B))) by A2

        .= ((N . A) + (N . B)) by A2;

      end;

      then

       A9: N is additive by MEASURE1:def 8;

      (N . {} ) = (M . (F " {} )) by A2, PROB_1: 4

      .= 0 by VALUED_0:def 19;

      then N is zeroed by VALUED_0:def 19;

      hence thesis by A3, A4, A9;

    end;

    definition

      let Omega1, Omega2, S1, S2;

      let M be Measure of S1, F be random_variable of S1, S2;

      :: RANDOM_3:def6

      func image_measure (F,M) -> Measure of S2 means

      : Def6: for y be Element of S2 holds (it . y) = (M . (F " y));

      existence by Lm2;

      uniqueness

      proof

        let N1,N2 be Measure of S2;

        assume

         A1: for y be Element of S2 holds (N1 . y) = (M . (F " y));

        assume

         A2: for y be Element of S2 holds (N2 . y) = (M . (F " y));

        now

          let y be Element of S2;

          

          thus (N1 . y) = (M . (F " y)) by A1

          .= (N2 . y) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      let Omega1, Omega2, S1, S2;

      let M be sigma_Measure of S1, F be random_variable of S1, S2;

      cluster ( image_measure (F,M)) -> sigma-additive;

      coherence

      proof

        set N = ( image_measure (F,M));

        for s2 be Sep_Sequence of S2 holds ( SUM (N * s2)) = (N . ( union ( rng s2)))

        proof

          let s2 be Sep_Sequence of S2;

          

           A1: for x,y be object st x <> y holds ((( " F) * s2) . x) misses ((( " F) * s2) . y)

          proof

            let x,y be object;

            assume

             A2: x <> y;

            

             A3: ((F " (s2 . x)) /\ (F " (s2 . y))) = (F " ((s2 . x) /\ (s2 . y))) by FUNCT_1: 68

            .= (F " {} ) by A2, XBOOLE_0:def 7, PROB_2:def 2

            .= {} ;

            per cases ;

              suppose

               A4: x in ( dom (( " F) * s2)) & y in ( dom (( " F) * s2));

              then

               A5: x in ( dom s2) & (s2 . x) in ( dom ( " F)) by FUNCT_1: 11;

              

               A6: y in ( dom s2) & (s2 . y) in ( dom ( " F)) by A4, FUNCT_1: 11;

              

               A7: ((( " F) * s2) . x) = (( " F) . (s2 . x)) by A4, FUNCT_1: 12

              .= (F " (s2 . x)) by MEASURE6:def 3, A5;

              ((( " F) * s2) . y) = (( " F) . (s2 . y)) by A4, FUNCT_1: 12

              .= (F " (s2 . y)) by A6, MEASURE6:def 3;

              hence ((( " F) * s2) . x) misses ((( " F) * s2) . y) by A7, A3;

            end;

              suppose not (x in ( dom (( " F) * s2)) & y in ( dom (( " F) * s2)));

              then ((( " F) * s2) . x) = {} or ((( " F) * s2) . y) = {} by FUNCT_1:def 2;

              hence ((( " F) * s2) . x) misses ((( " F) * s2) . y);

            end;

          end;

          s2 in ( Funcs ( NAT ,S2)) by FUNCT_2: 8;

          then ex f be Function st s2 = f & ( dom f) = NAT & ( rng f) c= S2 by FUNCT_2:def 2;

          then

           A8: ( dom s2) = NAT & ( rng s2) c= S2;

          

           A9: ( dom ( " F)) = ( bool Omega2) by FUNCT_2:def 1;

          then

           A10: ( dom (( " F) * s2)) = NAT by A8, RELAT_1: 27;

          

           A11: for x be object st x in NAT holds ((( " F) * s2) . x) in S1

          proof

            let x be object;

            assume x in NAT ;

            then

            reconsider n = x as Element of NAT ;

            per cases ;

              suppose

               A12: n in ( dom (( " F) * s2));

              then

               A13: n in ( dom s2) & (s2 . n) in ( dom ( " F)) by FUNCT_1: 11;

              ((( " F) * s2) . n) = (( " F) . (s2 . n)) by A12, FUNCT_1: 12

              .= (F " (s2 . n)) by A13, MEASURE6:def 3;

              hence ((( " F) * s2) . x) in S1 by FINANCE1:def 5;

            end;

              suppose not n in ( dom (( " F) * s2));

              then ((( " F) * s2) . n) = {} by FUNCT_1:def 2;

              hence ((( " F) * s2) . x) in S1 by PROB_1: 4;

            end;

          end;

          then

           A14: (( " F) * s2) is Function of NAT , S1 by A10, FUNCT_2: 3;

          reconsider s1 = (( " F) * s2) as Sep_Sequence of S1 by A1, PROB_2:def 2, A10, FUNCT_2: 3, A11;

          

           A15: ( SUM (M * s1)) = (M . ( union ( rng s1))) by MEASURE1:def 6;

          now

            let n be Element of NAT ;

            

             A16: ((M * s1) . n) = (M . (s1 . n)) by FUNCT_2: 15;

            

             A17: ((N * s2) . n) = (N . (s2 . n)) by FUNCT_2: 15;

            per cases ;

              suppose

               A18: n in ( dom (( " F) * s2));

              then

               A19: n in ( dom s2) & (s2 . n) in ( dom ( " F)) by FUNCT_1: 11;

              

               A20: (s1 . n) = (( " F) . (s2 . n)) by A18, FUNCT_1: 12

              .= (F " (s2 . n)) by A19, MEASURE6:def 3;

              

              thus ((M * s1) . n) = (M . (F " (s2 . n))) by A20, FUNCT_2: 15

              .= (N . (s2 . n)) by Def6

              .= ((N * s2) . n) by FUNCT_2: 15;

            end;

              suppose

               A21: not n in ( dom (( " F) * s2));

              

               A22: ((M * s1) . n) = (M . {} ) by A21, A16, FUNCT_1:def 2

              .= 0 by VALUED_0:def 19;

              

               A23: not n in ( dom s2) or not (s2 . n) in ( dom ( " F)) by A21, FUNCT_1: 11;

              (s2 . n) in S2;

              then (s2 . n) = {} by FUNCT_1:def 2, A23, A9;

              hence ((M * s1) . n) = ((N * s2) . n) by A22, A17, VALUED_0:def 19;

            end;

          end;

          then

           A24: (M * s1) = (N * s2) by FUNCT_2:def 8;

          for x be object holds x in ( union ( rng (( " F) * s2))) iff x in (F " ( union ( rng s2)))

          proof

            let x be object;

            hereby

              assume x in ( union ( rng (( " F) * s2)));

              then

              consider Y be set such that

               A25: x in Y & Y in ( rng (( " F) * s2)) by TARSKI:def 4;

              consider n be Element of NAT such that

               A26: Y = ((( " F) * s2) . n) by A25, A14, FUNCT_2: 113;

              

               A27: n in ( dom s2) & (s2 . n) in ( dom ( " F)) by FUNCT_1: 11, A10;

              

               A28: ((( " F) * s2) . n) = (( " F) . (s2 . n)) by A10, FUNCT_1: 12

              .= (F " (s2 . n)) by A27, MEASURE6:def 3;

              (s2 . n) c= ( union ( rng s2)) by ZFMISC_1: 74, FUNCT_2: 4;

              then (F " (s2 . n)) c= (F " ( union ( rng s2))) by RELAT_1: 143;

              hence x in (F " ( union ( rng s2))) by A25, A26, A28;

            end;

            assume x in (F " ( union ( rng s2)));

            then

             A29: x in ( dom F) & (F . x) in ( union ( rng s2)) by FUNCT_1:def 7;

            then

            consider Z be set such that

             A30: (F . x) in Z & Z in ( rng s2) by TARSKI:def 4;

            consider n be Element of NAT such that

             A31: Z = (s2 . n) by A30, FUNCT_2: 113;

            

             A32: x in (F " Z) by A30, FUNCT_1:def 7, A29;

            

             A33: n in ( dom s2) & (s2 . n) in ( dom ( " F)) by FUNCT_1: 11, A10;

            

             A34: ((( " F) * s2) . n) = (( " F) . (s2 . n)) by A10, FUNCT_1: 12

            .= (F " (s2 . n)) by A33, MEASURE6:def 3;

            (F " Z) in ( rng (( " F) * s2)) by A31, A10, A34, FUNCT_1: 3;

            hence x in ( union ( rng (( " F) * s2))) by A32, TARSKI:def 4;

          end;

          then

           A35: ( union ( rng (( " F) * s2))) = (F " ( union ( rng s2))) by TARSKI: 2;

          ( union ( rng s2)) is Element of S2 by MEASURE1: 24;

          hence thesis by A15, A24, A35, Def6;

        end;

        hence thesis by MEASURE1:def 6;

      end;

    end

    theorem :: RANDOM_3:12

    

     Th12: for P be Probability of S1, F be random_variable of S1, S2 holds (( image_measure (F,( P2M P))) . Omega2) = 1

    proof

      let P be Probability of S1, F be random_variable of S1, S2;

      

       A1: for y be set st y in S2 holds (( image_measure (F,( P2M P))) . y) = (( P2M P) . (F " y)) by Def6;

      

      thus (( image_measure (F,( P2M P))) . Omega2) = (( P2M P) . (F " Omega2)) by PROB_1: 5, A1

      .= (( P2M P) . Omega1) by FUNCT_2: 40

      .= 1 by PROB_1:def 8;

    end;

    definition

      let Omega1, Omega2, S1, S2;

      let P be Probability of S1, F be random_variable of S1, S2;

      :: RANDOM_3:def7

      func probability (F,P) -> Probability of S2 equals ( M2P ( image_measure (F,( P2M P))));

      coherence ;

    end

    theorem :: RANDOM_3:13

    

     Th13: for P be Probability of S1, F be random_variable of S1, S2 holds ( probability (F,P)) = ( image_measure (F,( P2M P)))

    proof

      let P be Probability of S1, F be random_variable of S1, S2;

      (( image_measure (F,( P2M P))) . Omega2) = 1 by Th12;

      hence ( probability (F,P)) = ( image_measure (F,( P2M P))) by PROB_4:def 2;

    end;

    theorem :: RANDOM_3:14

    

     Th14: for P be Probability of S1, F be random_variable of S1, S2 holds for y be set st y in S2 holds (( probability (F,P)) . y) = (P . (F " y))

    proof

      let P be Probability of S1, F be random_variable of S1, S2;

      let y be set;

      assume

       A1: y in S2;

      

      thus (( probability (F,P)) . y) = (( image_measure (F,( P2M P))) . y) by Th13

      .= (P . (F " y)) by A1, Def6;

    end;

    theorem :: RANDOM_3:15

    

     Th15: for F be Function of Omega1, Omega2 holds F is random_variable of ( Trivial-SigmaField Omega1), ( Trivial-SigmaField Omega2)

    proof

      let F be Function of Omega1, Omega2;

      set S1 = ( Trivial-SigmaField Omega1);

      set S2 = ( Trivial-SigmaField Omega2);

      for y be set st y in S2 holds (F " y) in S1;

      hence thesis by FINANCE1:def 5;

    end;

    theorem :: RANDOM_3:16

    

     Th16: for S be non empty set, F be non empty FinSequence of S holds F is random_variable of ( Trivial-SigmaField ( Seg ( len F))), ( Trivial-SigmaField S)

    proof

      let S be non empty set, F be non empty FinSequence of S;

      reconsider n = ( len F) as non empty Element of NAT ;

      

       A1: ( dom F) = ( Seg n) by FINSEQ_1:def 3;

      ( rng F) c= S;

      hence thesis by Th15, A1, FUNCT_2: 2;

    end;

    theorem :: RANDOM_3:17

    

     Th17: for V,S be finite non empty set, G be random_variable of ( Trivial-SigmaField V), ( Trivial-SigmaField S) holds for y be set st y in ( Trivial-SigmaField S) holds (( probability (G,( Trivial-Probability V))) . y) = (( card (G " y)) / ( card V))

    proof

      let V,S be finite non empty set, G be random_variable of ( Trivial-SigmaField V), ( Trivial-SigmaField S);

      now

        let y be set;

        assume

         A1: y in ( Trivial-SigmaField S);

        

        thus (( probability (G,( Trivial-Probability V))) . y) = (( Trivial-Probability V) . (G " y)) by Th14, A1

        .= ( prob (G " y)) by RANDOM_1:def 1

        .= (( card (G " y)) / ( card V));

      end;

      hence thesis;

    end;

    theorem :: RANDOM_3:18

    for S be finite non empty set, s be non empty FinSequence of S holds ex G be random_variable of ( Trivial-SigmaField ( Seg ( len s))), ( Trivial-SigmaField S) st G = s & for x be set st x in S holds (( probability (G,( Trivial-Probability ( Seg ( len s))))) . {x}) = ( FDprobability (x,s))

    proof

      let S be finite non empty set, s be non empty FinSequence of S;

      reconsider n = ( len s) as non empty Element of NAT ;

      reconsider G = s as random_variable of ( Trivial-SigmaField ( Seg ( len s))), ( Trivial-SigmaField S) by Th16;

      take G;

      thus G = s;

      let x be set;

      assume

       A1: x in S;

      set y = {x};

       {x} c= S by A1, ZFMISC_1: 31;

      

      then (( probability (G,( Trivial-Probability ( Seg ( len s))))) . y) = (( card (G " y)) / ( card ( Seg ( len s)))) by Th17

      .= (( card (G " y)) / n) by FINSEQ_1: 57;

      hence thesis;

    end;

    begin

    registration

      let D be non-empty ManySortedSet of NAT ;

      let n be Nat;

      cluster (D . n) -> non empty;

      correctness

      proof

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

        (D . n1) is non empty set;

        hence thesis;

      end;

    end

    definition

      let S,F be ManySortedSet of NAT ;

      :: RANDOM_3:def8

      attr F is S -SigmaField_sequence-like means

      : Def8: for n be Nat holds (F . n) is SigmaField of (S . n);

    end

    registration

      let S be ManySortedSet of NAT ;

      cluster S -SigmaField_sequence-like for ManySortedSet of NAT ;

      existence

      proof

        defpred P[ set, set] means $2 is SigmaField of (S . $1);

        set X = ( union ( rng S));

        

         A1: for n be Element of NAT holds ex y be Element of ( bool ( bool X)) st P[n, y]

        proof

          let n be Element of NAT ;

          set y = the SigmaField of (S . n);

          ( dom S) = NAT by PARTFUN1:def 2;

          then (S . n) in ( rng S) by FUNCT_1: 3;

          then ( bool (S . n)) c= ( bool X) by ZFMISC_1: 67, ZFMISC_1: 74;

          hence thesis;

        end;

        consider F be Function of NAT , ( bool ( bool X)) such that

         A2: for n be Element of NAT holds P[n, (F . n)] from FUNCT_2:sch 3( A1);

        take F;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence (F . n) is SigmaField of (S . n) by A2;

      end;

    end

    definition

      let D be ManySortedSet of NAT ;

      mode SigmaField_sequence of D is D -SigmaField_sequence-like ManySortedSet of NAT ;

    end

    definition

      let D be ManySortedSet of NAT ;

      let S be SigmaField_sequence of D;

      let n be Nat;

      :: original: .

      redefine

      func S . n -> SigmaField of (D . n) ;

      correctness by Def8;

    end

    definition

      let D be non-empty ManySortedSet of NAT ;

      let S be SigmaField_sequence of D;

      let M be ManySortedSet of NAT ;

      :: RANDOM_3:def9

      attr M is S -Probability_sequence-like means

      : Def9: for n be Nat holds (M . n) is Probability of (S . n);

    end

    registration

      let D be non-empty ManySortedSet of NAT ;

      let S be SigmaField_sequence of D;

      cluster S -Probability_sequence-like for ManySortedSet of NAT ;

      existence

      proof

        defpred P[ set, set] means ex Dn be non empty set, Sn be SigmaField of Dn st Dn = (D . $1) & Sn = (S . $1) & $2 is Probability of Sn;

        set X = ( union ( rng S));

        

         A1: for n be Element of NAT holds ex y be Element of ( PFuncs (X, REAL )) st P[n, y]

        proof

          let n be Element of NAT ;

          ( dom S) = NAT by PARTFUN1:def 2;

          then

           A2: (S . n) c= X by ZFMISC_1: 74, FUNCT_1: 3;

          reconsider Sn = (S . n) as SigmaField of (D . n);

          set Mn = the Probability of Sn;

          Mn in ( Funcs ((S . n), REAL )) by FUNCT_2: 8;

          then ex f be Function st Mn = f & ( dom f) = (S . n) & ( rng f) c= REAL by FUNCT_2:def 2;

          then Mn in ( PFuncs (X, REAL )) by PARTFUN1:def 3, A2;

          hence thesis;

        end;

        consider F be Function of NAT , ( PFuncs (X, REAL )) such that

         A3: for n be Element of NAT holds P[n, (F . n)] from FUNCT_2:sch 3( A1);

        take F;

        let n be Nat;

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

        ex Dn be non empty set, Sn be SigmaField of Dn st Dn = (D . n1) & Sn = (S . n1) & (F . n1) is Probability of Sn by A3;

        hence thesis;

      end;

    end

    definition

      let D be non-empty ManySortedSet of NAT ;

      let S be SigmaField_sequence of D;

      mode Probability_sequence of S is S -Probability_sequence-like ManySortedSet of NAT ;

    end

    definition

      let D be non-empty ManySortedSet of NAT ;

      let S be SigmaField_sequence of D;

      let P be Probability_sequence of S;

      let n be Nat;

      :: original: .

      redefine

      func P . n -> Probability of (S . n) ;

      correctness by Def9;

    end

    definition

      let D be ManySortedSet of NAT ;

      :: RANDOM_3:def10

      func Product_dom (D) -> ManySortedSet of NAT means

      : Def10: (it . 0 ) = (D . 0 ) & for i be Nat holds (it . (i + 1)) = [:(it . i), (D . (i + 1)):];

      existence

      proof

        defpred R[ Nat, set, set] means $3 = [:$2, (D . ($1 + 1)):];

        

         A1: for n be Nat holds for x be set holds ex y be set st R[n, x, y];

        consider g be Function such that

         A2: ( dom g) = NAT & (g . 0 ) = (D . 0 ) & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A1);

        reconsider g as ManySortedSet of NAT by PARTFUN1:def 2, RELAT_1:def 18, A2;

        take g;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let seq1,seq2 be ManySortedSet of NAT ;

        assume that

         A3: (seq1 . 0 ) = (D . 0 ) and

         A4: for i be Nat holds (seq1 . (i + 1)) = [:(seq1 . i), (D . (i + 1)):] and

         A5: (seq2 . 0 ) = (D . 0 ) and

         A6: for i be Nat holds (seq2 . (i + 1)) = [:(seq2 . i), (D . (i + 1)):];

        

         A7: ( dom seq2) = NAT by PARTFUN1:def 2;

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

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

        proof

          let k be Nat;

          assume

           A9: P[k];

          

          thus (seq1 . (k + 1)) = [:(seq1 . k), (D . (k + 1)):] by A4

          .= (seq2 . (k + 1)) by A6, A9;

        end;

        

         A10: P[ 0 ] by A3, A5;

        

         A11: for n be Nat holds P[n] from NAT_1:sch 2( A10, A8);

        for n be object st n in ( dom seq1) holds (seq1 . n) = (seq2 . n) by A11;

        hence seq1 = seq2 by A7, FUNCT_1: 2, PARTFUN1:def 2;

      end;

    end

    theorem :: RANDOM_3:19

    

     Th19: for D be ManySortedSet of NAT holds (( Product_dom D) . 0 ) = (D . 0 ) & (( Product_dom D) . 1) = [:(D . 0 ), (D . 1):] & (( Product_dom D) . 2) = [:(D . 0 ), (D . 1), (D . 2):] & (( Product_dom D) . 3) = [:(D . 0 ), (D . 1), (D . 2), (D . 3):]

    proof

      let D be ManySortedSet of NAT ;

      thus (( Product_dom D) . 0 ) = (D . 0 ) by Def10;

      

      thus

       A1: (( Product_dom D) . 1) = (( Product_dom D) . ( 0 qua Nat + 1))

      .= [:(( Product_dom D) . 0 ), (D . 1):] by Def10

      .= [:(D . 0 ), (D . 1):] by Def10;

      

      thus

       A2: (( Product_dom D) . 2) = [:(( Product_dom D) . 1), (D . (1 + 1)):] by Def10

      .= [:(D . 0 ), (D . 1), (D . 2):] by ZFMISC_1:def 3, A1;

      

      thus (( Product_dom D) . 3) = [:(( Product_dom D) . 2), (D . (2 + 1)):] by Def10

      .= [:(D . 0 ), (D . 1), (D . 2), (D . 3):] by ZFMISC_1:def 4, A2;

    end;

    registration

      let D be non-empty ManySortedSet of NAT ;

      cluster ( Product_dom D) -> non-empty;

      correctness

      proof

        set g = ( Product_dom D);

        defpred P[ Nat] means (g . $1) is non empty;

        (D . 0 ) = (( Product_dom D) . 0 ) by Def10;

        then

         A1: P[ 0 ];

        

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

        proof

          let k be Nat;

          (g . (k + 1)) = [:(g . k), (D . (k + 1)):] by Def10;

          hence thesis;

        end;

        

         A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

        assume not g is non-empty;

        then {} in ( rng g);

        then ex x be object st x in ( dom g) & {} = (g . x) by FUNCT_1:def 3;

        hence contradiction by A3;

      end;

    end

    registration

      let D be finite-yielding ManySortedSet of NAT ;

      cluster ( Product_dom D) -> finite-yielding;

      correctness

      proof

        set g = ( Product_dom D);

        defpred P[ Nat] means (g . $1) is finite;

        (D . 0 ) = (( Product_dom D) . 0 ) by Def10;

        then

         A1: P[ 0 ];

        

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

        proof

          let k be Nat;

          (g . (k + 1)) = [:(g . k), (D . (k + 1)):] by Def10;

          hence thesis;

        end;

        

         A3: for n be Nat holds P[n] from NAT_1:sch 2( A1, A2);

        let x be object;

        thus thesis by A3;

      end;

    end

    definition

      let Omega, Sigma;

      let P be set;

      assume

       A1: P is Probability of Sigma;

      :: RANDOM_3:def11

      func modetrans (P,Sigma) -> Probability of Sigma equals

      : Def11: P;

      correctness by A1;

    end

    definition

      let D be finite-yielding non-empty ManySortedSet of NAT ;

      :: RANDOM_3:def12

      func Trivial-SigmaField_sequence (D) -> SigmaField_sequence of D means

      : Def12: for n be Nat holds (it . n) = ( Trivial-SigmaField (D . n));

      existence

      proof

        deffunc F( Nat) = ( Trivial-SigmaField (D . $1));

        consider f be Function such that

         A1: ( dom f) = NAT & for x be Element of NAT holds (f . x) = F(x) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of NAT by A1, PARTFUN1:def 2, RELAT_1:def 18;

        now

          let n be Nat;

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

          (f . n1) = ( Trivial-SigmaField (D . n1)) by A1;

          hence (f . n) is SigmaField of (D . n);

        end;

        then

        reconsider f as SigmaField_sequence of D by Def8;

        take f;

        now

          let n be Nat;

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

          (f . n1) = ( Trivial-SigmaField (D . n1)) by A1;

          hence (f . n) = ( Trivial-SigmaField (D . n));

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let seq1,seq2 be SigmaField_sequence of D;

        assume that

         A2: for n be Nat holds (seq1 . n) = ( Trivial-SigmaField (D . n)) and

         A3: for n be Nat holds (seq2 . n) = ( Trivial-SigmaField (D . n));

        

         A4: ( dom seq2) = NAT by PARTFUN1:def 2;

        now

          let n be object;

          assume n in ( dom seq1);

          then

          reconsider i = n as Nat;

          

          thus (seq1 . n) = ( Trivial-SigmaField (D . i)) by A2

          .= (seq2 . n) by A3;

        end;

        hence seq1 = seq2 by A4, FUNCT_1: 2, PARTFUN1:def 2;

      end;

    end

    definition

      let D be finite-yielding non-empty ManySortedSet of NAT ;

      let P be Probability_sequence of ( Trivial-SigmaField_sequence D);

      let n be Nat;

      :: original: .

      redefine

      func P . n -> Probability of ( Trivial-SigmaField (D . n)) ;

      coherence

      proof

        (P . n) is Probability of (( Trivial-SigmaField_sequence D) . n);

        hence thesis by Def12;

      end;

    end

    definition

      let D be finite-yielding non-empty ManySortedSet of NAT ;

      let P be Probability_sequence of ( Trivial-SigmaField_sequence D);

      :: RANDOM_3:def13

      func Product-Probability (P,D) -> ManySortedSet of NAT means

      : Def13: (it . 0 ) = (P . 0 ) & for i be Nat holds (it . (i + 1)) = ( Product-Probability ((( Product_dom D) . i),(D . (i + 1)),( modetrans ((it . i),( Trivial-SigmaField (( Product_dom D) . i)))),(P . (i + 1))));

      existence

      proof

        defpred R[ Nat, set, set] means $3 = ( Product-Probability ((( Product_dom D) . $1),(D . ($1 + 1)),( modetrans ($2,( Trivial-SigmaField (( Product_dom D) . $1)))),(P . ($1 + 1))));

        

         A1: for n be Nat holds for x be set holds ex y be set st R[n, x, y];

        consider g be Function such that

         A2: ( dom g) = NAT & (g . 0 ) = (P . 0 ) & for n be Nat holds R[n, (g . n), (g . (n + 1))] from RECDEF_1:sch 1( A1);

        reconsider g as NAT -defined Function by RELAT_1:def 18, A2;

        reconsider g as ManySortedSet of NAT by PARTFUN1:def 2, A2;

        take g;

        thus (g . 0 ) = (P . 0 ) by A2;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let seq1,seq2 be ManySortedSet of NAT ;

        assume that

         A3: (seq1 . 0 ) = (P . 0 ) and

         A4: for i be Nat holds (seq1 . (i + 1)) = ( Product-Probability ((( Product_dom D) . i),(D . (i + 1)),( modetrans ((seq1 . i),( Trivial-SigmaField (( Product_dom D) . i)))),(P . (i + 1)))) and

         A5: (seq2 . 0 ) = (P . 0 ) and

         A6: for i be Nat holds (seq2 . (i + 1)) = ( Product-Probability ((( Product_dom D) . i),(D . (i + 1)),( modetrans ((seq2 . i),( Trivial-SigmaField (( Product_dom D) . i)))),(P . (i + 1))));

        

         A7: ( dom seq2) = NAT by PARTFUN1:def 2;

        defpred P[ Nat] means (seq1 . $1) = (seq2 . $1);

        

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

        proof

          let k be Nat;

          assume

           A9: P[k];

          

          thus (seq1 . (k + 1)) = ( Product-Probability ((( Product_dom D) . k),(D . (k + 1)),( modetrans ((seq2 . k),( Trivial-SigmaField (( Product_dom D) . k)))),(P . (k + 1)))) by A9, A4

          .= (seq2 . (k + 1)) by A6;

        end;

        

         A10: P[ 0 ] by A3, A5;

        for n be Nat holds P[n] from NAT_1:sch 2( A10, A8);

        then for n be object st n in ( dom seq1) holds (seq1 . n) = (seq2 . n);

        hence seq1 = seq2 by A7, FUNCT_1: 2, PARTFUN1:def 2;

      end;

    end

    theorem :: RANDOM_3:20

    

     Th20: for D be finite-yielding non-empty ManySortedSet of NAT , P be Probability_sequence of ( Trivial-SigmaField_sequence D), n be Nat holds (( Product-Probability (P,D)) . n) is Probability of ( Trivial-SigmaField (( Product_dom D) . n))

    proof

      let D be finite-yielding non-empty ManySortedSet of NAT , P be Probability_sequence of ( Trivial-SigmaField_sequence D);

      defpred Q[ Nat] means (( Product-Probability (P,D)) . $1) is Probability of ( Trivial-SigmaField (( Product_dom D) . $1));

      

       A1: (( Product-Probability (P,D)) . 0 ) = (P . 0 ) by Def13;

      (D . 0 ) = (( Product_dom D) . 0 ) by Def10;

      then

       A2: Q[ 0 ] by A1;

      

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

      proof

        let k be Nat;

        assume Q[k];

        

         A4: (( Product-Probability (P,D)) . (k + 1)) = ( Product-Probability ((( Product_dom D) . k),(D . (k + 1)),( modetrans ((( Product-Probability (P,D)) . k),( Trivial-SigmaField (( Product_dom D) . k)))),(P . (k + 1)))) by Def13;

        (( Product_dom D) . (k + 1)) = [:(( Product_dom D) . k), (D . (k + 1)):] by Def10;

        hence thesis by A4;

      end;

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

      hence thesis;

    end;

    theorem :: RANDOM_3:21

    

     Th21: for D be finite-yielding non-empty ManySortedSet of NAT , P be Probability_sequence of ( Trivial-SigmaField_sequence D), n be Nat holds ex Pn be Probability of ( Trivial-SigmaField (( Product_dom D) . n)) st Pn = (( Product-Probability (P,D)) . n) & (( Product-Probability (P,D)) . (n + 1)) = ( Product-Probability ((( Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))))

    proof

      let D be finite-yielding non-empty ManySortedSet of NAT , P be Probability_sequence of ( Trivial-SigmaField_sequence D), n be Nat;

      reconsider Pn = (( Product-Probability (P,D)) . n) as Probability of ( Trivial-SigmaField (( Product_dom D) . n)) by Th20;

      take Pn;

      thus Pn = (( Product-Probability (P,D)) . n);

      

      thus (( Product-Probability (P,D)) . (n + 1)) = ( Product-Probability ((( Product_dom D) . n),(D . (n + 1)),( modetrans ((( Product-Probability (P,D)) . n),( Trivial-SigmaField (( Product_dom D) . n)))),(P . (n + 1)))) by Def13

      .= ( Product-Probability ((( Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1)))) by Def11;

    end;

    theorem :: RANDOM_3:22

    for D be finite-yielding non-empty ManySortedSet of NAT , P be Probability_sequence of ( Trivial-SigmaField_sequence D) holds (( Product-Probability (P,D)) . 0 ) = (P . 0 ) & (( Product-Probability (P,D)) . 1) = ( Product-Probability ((D . 0 ),(D . 1),(P . 0 ),(P . 1))) & (ex P1 be Probability of ( Trivial-SigmaField [:(D . 0 ), (D . 1):]) st P1 = (( Product-Probability (P,D)) . 1) & (( Product-Probability (P,D)) . 2) = ( Product-Probability ( [:(D . 0 ), (D . 1):],(D . 2),P1,(P . 2)))) & (ex P2 be Probability of ( Trivial-SigmaField [:(D . 0 ), (D . 1), (D . 2):]) st P2 = (( Product-Probability (P,D)) . 2) & (( Product-Probability (P,D)) . 3) = ( Product-Probability ( [:(D . 0 ), (D . 1), (D . 2):],(D . 3),P2,(P . 3)))) & (ex P3 be Probability of ( Trivial-SigmaField [:(D . 0 ), (D . 1), (D . 2), (D . 3):]) st P3 = (( Product-Probability (P,D)) . 3) & (( Product-Probability (P,D)) . 4) = ( Product-Probability ( [:(D . 0 ), (D . 1), (D . 2), (D . 3):],(D . 4),P3,(P . 4))))

    proof

      let D be finite-yielding non-empty ManySortedSet of NAT , P be Probability_sequence of ( Trivial-SigmaField_sequence D);

      thus (( Product-Probability (P,D)) . 0 ) = (P . 0 ) by Def13;

      

       A1: (( Product_dom D) . 0 ) = (D . 0 ) by Th19;

      

       A2: ( modetrans ((( Product-Probability (P,D)) . 0 ),( Trivial-SigmaField (( Product_dom D) . 0 )))) = ( modetrans ((P . 0 ),( Trivial-SigmaField (D . 0 )))) by A1, Def13

      .= (P . 0 ) by Def11;

      

      thus (( Product-Probability (P,D)) . 1) = (( Product-Probability (P,D)) . ( 0 qua Nat + 1))

      .= ( Product-Probability ((( Product_dom D) . 0 ),(D . 1),( modetrans ((( Product-Probability (P,D)) . 0 ),( Trivial-SigmaField (( Product_dom D) . 0 )))),(P . 1))) by Def13

      .= ( Product-Probability ((D . 0 ),(D . 1),(P . 0 ),(P . 1))) by A2, Th19;

      consider P1 be Probability of ( Trivial-SigmaField (( Product_dom D) . 1)) such that

       A3: P1 = (( Product-Probability (P,D)) . 1) & (( Product-Probability (P,D)) . (1 + 1)) = ( Product-Probability ((( Product_dom D) . 1),(D . (1 + 1)),P1,(P . (1 + 1)))) by Th21;

      (( Product_dom D) . 1) = [:(D . 0 ), (D . 1):] by Th19;

      then

      reconsider P1 as Probability of ( Trivial-SigmaField [:(D . 0 ), (D . 1):]);

      

       A4: (( Product-Probability (P,D)) . 2) = ( Product-Probability ( [:(D . 0 ), (D . 1):],(D . 2),P1,(P . 2))) by A3, Th19;

      consider P2 be Probability of ( Trivial-SigmaField (( Product_dom D) . 2)) such that

       A5: P2 = (( Product-Probability (P,D)) . 2) & (( Product-Probability (P,D)) . (2 + 1)) = ( Product-Probability ((( Product_dom D) . 2),(D . (2 + 1)),P2,(P . (2 + 1)))) by Th21;

      (( Product_dom D) . 2) = [:(D . 0 ), (D . 1), (D . 2):] by Th19;

      then

      reconsider P2 as Probability of ( Trivial-SigmaField [:(D . 0 ), (D . 1), (D . 2):]);

      

       A6: (( Product-Probability (P,D)) . 3) = ( Product-Probability ( [:(D . 0 ), (D . 1), (D . 2):],(D . 3),P2,(P . 3))) by A5, Th19;

      consider P3 be Probability of ( Trivial-SigmaField (( Product_dom D) . 3)) such that

       A7: P3 = (( Product-Probability (P,D)) . 3) & (( Product-Probability (P,D)) . (3 + 1)) = ( Product-Probability ((( Product_dom D) . 3),(D . (3 + 1)),P3,(P . (3 + 1)))) by Th21;

      (( Product_dom D) . 3) = [:(D . 0 ), (D . 1), (D . 2), (D . 3):] by Th19;

      then

      reconsider P3 as Probability of ( Trivial-SigmaField [:(D . 0 ), (D . 1), (D . 2), (D . 3):]);

      (( Product-Probability (P,D)) . 4) = ( Product-Probability ( [:(D . 0 ), (D . 1), (D . 2), (D . 3):],(D . 4),P3,(P . 4))) by A7, Th19;

      hence thesis by A4, A5, A3, A7, A6;

    end;