:: Random Variables and Product of Probability Spaces
::  by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 1, 2012
:: Copyright (c) 2012-2018 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, TARSKI,
      RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, XXREAL_1, LOPBAN_1, FUNCT_2, DIST_1,
      MSSUBFAM, VALUED_0, MESFUNC1, SUPINF_2, FINSEQ_1, NAT_1, CARD_3, CARD_1,
      ZFMISC_1, RPR_1, FINSET_1, PROB_4, EQREL_1, RANDOM_1, RANDOM_2, RANDOM_3,
      FUNCOP_1, FINANCE1, PBOOLE, REAL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PBOOLE, ENUMSET1,
      FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_1, NAT_1, XREAL_0,
      VALUED_0, FINSEQ_1, RPR_1, SUPINF_2, PROB_1, PROB_2, MEASURE1, MEASURE6,
      MESFUNC1, PROB_4, MESFUNC6, RANDOM_1, DIST_1, RANDOM_2, FINANCE1;
 constructors REAL_1, RPR_1, MESFUNC6, MESFUNC3, DIST_1, MEASURE6, INTEGRA2,
      PROB_4, MESFUNC1, RELSET_1, COMSEQ_2, RANDOM_2, FINANCE1, ENUMSET1;
 registrations XBOOLE_0, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1,
      MEASURE1, FUNCOP_1, FINANCE1, VALUED_0, FINSEQ_1, FUNCT_2, RELAT_1,
      PROB_2, FINSET_1, NUMBERS, PROB_1, PARTFUN1, RELSET_1, CARD_1, PBOOLE,
      PRE_CIRC;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0, FINSET_1;
 equalities RPR_1, SUBSET_1, RANDOM_2, PROB_4, PROB_1, RELAT_1, DIST_1,
      FINANCE1, CARD_3;
 expansions TARSKI, XBOOLE_0, RELAT_1, FINANCE1;
 theorems TARSKI, PARTFUN1, FUNCT_1, MESFUNC1, FINSEQ_1, XBOOLE_0, XBOOLE_1,
      PROB_2, XXREAL_0, PROB_1, RELAT_1, ZFMISC_1, FUNCT_2, MEASURE1, PROB_4,
      MESFUNC6, MEASURE6, ORDINAL1, VALUED_0, RCOMP_1, FUNCOP_1, RANDOM_1,
      FINANCE1;
 schemes FUNCT_1, FUNCT_2, NAT_1, RECDEF_1;

begin :: Random Variables

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 Th1:
  for B being non empty set, f being Function holds
  f " (union B)
  = union the set of all f "Y where Y is Element of B
  proof
    let B be non empty set, f be Function;
    set Z = the set of all f "Y where Y is 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 being 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 being 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 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 is 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 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 is Element of NAT;
    set Q = the set of all f "Y where Y is 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 Th4:
  for F being Function of Omega,REAL,
  r being 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_measurable_on [#]Sigma 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 is 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 is 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 Th5:
  for F being Function of Omega,REAL st
  F is Real-Valued-Random-Variable of Sigma holds
  { x where x is 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 is 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 being 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 being 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 Th6:
  for f being Function of Omega,REAL
  st f is Real-Valued-Random-Variable of Sigma holds
  { x where x is 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 is 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 Th7:
  for f being Function of Omega,REAL holds
  f is_random_variable_on Sigma, Borel_Sets iff
  f is Real-Valued-Random-Variable of Sigma
  proof
    let f be Function of Omega,REAL;
    thus f is_random_variable_on Sigma, Borel_Sets 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 is Element of Borel_Sets : f"x is Element of Sigma };
    A2:B= Borel_Sets by Th6,A1;
    for x being 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
  for f being 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 being Function of Omega,REAL such that
        A1: x=f & f is_random_variable_on Sigma,Borel_Sets;
        f is_random_variable_on Sigma,Borel_Sets 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_random_variable_on Sigma, Borel_Sets by Th7;
      hence x in set_of_random_variables_on (Sigma,Borel_Sets) by A2;
    end;
    hence thesis by TARSKI:2;
  end;

definition
  let Omega1, Omega2, S1, S2;
  let F be Function of Omega1,Omega2;
  attr F is (S1,S2)-random_variable-like means :Def1:
  F is_random_variable_on S1,S2;
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_random_variable_on S1,S2;
    hence thesis by Def1;
  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
  for f being Function of Omega,REAL holds
  f is random_variable of Sigma, Borel_Sets iff
  f is Real-Valued-Random-Variable of Sigma by Th7,Def1;

definition
  let F be Function;
  attr F is random_variable_family-like means :Def2:
  for x be set st x in dom F
  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;
  attr F is S-Measure_valued means :Def3:
  for x be set st x in dom F ex M being 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 being 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;
  attr F is S-Probability_valued means :Def4:
  for x be set st x in dom F 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 being SigmaField of Y,
M be Probability of S
holds X --> M is S-Probability_valued
proof
  let X,Y be non empty set;
  let S be SigmaField of Y;
  let M be Probability of S;
  set F = X --> M;
  for x be set st x in dom F holds
  ex P being Probability of S st F.x = P by FUNCOP_1:7;
  hence thesis;
end;

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-defined S-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;
  attr F is S-Random-Variable-Family means :Def5:
  for x be set st x in dom F
  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 being Real-Valued-Random-Variable of S st F.x = Z by FUNCOP_1:7;
    hence thesis by Def5;
  end;
end;

theorem
  for y being Element of S2 st y <> {} holds
  {z where z is 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 is 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
  for F be random_variable of S1,S2 holds
  {x where x is Subset of Omega1 : ex y be Element of S2 st x =F"y } c= S1 &
  {x where x is 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 is 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,Def1,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 being 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
      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 being Function of NAT,bool Omega2 such that
      A11: for x being 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 being Measure of S1,
  F be random_variable of S1,S2
  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 Def1,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 Def1,FINANCE1:def 5;
      A8: F"B in S1 by Def1,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;
  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 being Sep_Sequence of S2 holds SUM(N*s2) = N.(union rng s2)
    proof
      let s2 be Sep_Sequence of S2;
      A1:for x, y being 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 being 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 Def1,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 Th12:
  for P being Probability of S1,
  F being 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;
  func probability(F,P) -> Probability of S2 equals
  M2P(image_measure(F,P2M(P)));
  coherence;
end;

theorem Th13:
  for P being Probability of S1,
  F being 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 Th14:
  for P being 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 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 being set st y in S2 holds F"y in S1;
    hence thesis by Def1,FINANCE1:def 5;
  end;

theorem 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 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
  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 :: Product of Probability Spaces

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;
  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 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 being 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;
  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;
  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 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 being 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 being 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;
  redefine func P.n -> Probability of (S.n);
  correctness by Def9;
end;

definition
  let D be ManySortedSet of NAT;
  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 being Nat for x be set ex y being set st R[n,x,y];
    consider g be Function such that
    A2: dom g = NAT & g.0 = D.0 &
    for n being 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 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;
  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;
  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;
  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);
  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 being Nat for x be set ex y being set st R[n,x,y];
    consider g be Function such that
    A2: dom g = NAT & g.0 = P.0 &
    for n being 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 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 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
  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;