:: Probability on Finite and Discrete Set and Uniform Distribution
::  by Hiroyuki Okazaki
:: 
:: Received May 5, 2009
:: Copyright (c) 2009 Association of Mizar Users

environ

 vocabularies DIST_1, FINSEQ_1, RELAT_1, SETFAM_1, FINSEQ_4, FUNCT_1, RPR_1,
      CARD_1, SEQ_1, BOOLE, ARYTM, TARSKI, ARYTM_3, RLVECT_1, PROB_1, PROB_2,
      FINSET_1, UPROOTS, MATRPROB, SEQM_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, CARD_1, ORDINAL1, NUMBERS,
      DOMAIN_1, XCMPLX_0, XXREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, FUNCT_2, BINOP_2, NAT_1,
      SETFAM_1, SEQ_1, RPR_1, PROB_2, RVSUM_1, UPROOTS, MATRPROB;
 constructors DOMAIN_1, RPR_1, RVSUM_1, SEQ_1, BINOP_2, SETWOP_2, PARTFUN3,
      INTEGRA2, PROB_2, VALUED_1, UPROOTS, MATRPROB, RELSET_1;
 registrations FUNCT_1, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, MEMBERED, ORDINAL1,
      UPROOTS, ALGSTR_0, FINSEQ_1, FUNCT_2, RELAT_1, XBOOLE_0, FINSET_1,
      NUMBERS, VALUED_0, VALUED_1, ASYMPT_0, CARD_1, MATRPROB, ENTROPY1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RPR_1, FINSEQ_1, RELAT_1, FUNCT_1;
 theorems XREAL_0, TARSKI, FINSEQ_2, CARD_2, FINSEQ_4, FUNCT_1, FINSEQ_1,
      XBOOLE_0, XBOOLE_1, XXREAL_0, PROB_2, NAT_1, RELAT_1, ZFMISC_1, FUNCT_2,
      XCMPLX_1, VALUED_1, UPROOTS, FINSEQ_5, CARD_1, RVSUM_1, MATRPROB;
 schemes NAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, SUBSET_1;

begin :: Probability on Finite and Discrete Set

notation
  let S be non empty finite set, s be FinSequence of S;
  synonym whole_event (s) for dom s;
end;

definition
  let S be non empty finite set, s be non empty FinSequence of S;
  redefine func whole_event (s) -> non empty finite set;
  correctness;
end;

theorem defwe:
  for S be non empty finite set, s be FinSequence of S
  holds whole_event (s) = s"S
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    P1: s"S c= s"rng s by RELAT_1:170;
    s"rng s c= s"S by RELAT_1:178;
    then
    s"rng s = s"S by P1,XBOOLE_0:def 10;
    hence thesis by RELAT_1:169;
  end;

notation let S be non empty finite set,
  s be FinSequence of S,
  x be set;
  synonym event_pick (x,s) for Coim(s,x);
end;

definition let S be non empty finite set, s be FinSequence of S, x be set;
  redefine func event_pick (x,s) -> Event of whole_event(s);
  correctness by RELAT_1:167;
end;

definition
  let S be non empty finite set, s be FinSequence of S, x be set;
  func frequency(x,s) -> Nat equals
    card (event_pick(x,s));
  correctness;
end;

theorem
  for S be non empty finite set,
  s be FinSequence of S, e be set st e in whole_event(s)
  ex x be Element of S st e in event_pick(x,s)
  proof
    let S be non empty finite set,
    s be FinSequence of S,
    e be set;
    assume AS: e in whole_event(s);
    then e in s"S by defwe;
    then s.e in S by FUNCT_1:def 13;
    then consider x be Element of S such that L1: x=s.e;
    CON: x in {x} by TARSKI:def 1;
    take x;
    thus thesis by CON,AS,L1,FUNCT_1:def 13;
  end;

theorem nazo6:
  for S be non empty finite set,
  s be FinSequence of S holds card whole_event(s) = len s
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    card whole_event(s)= card Seg len s by FINSEQ_1:def 3
    .= len s by FINSEQ_1:78;
    hence thesis;
  end;

definition let S be non empty finite set,
  s be FinSequence of S, x be set;
  func FDprobability (x,s) -> Real equals
  frequency(x,s) / (len s);
  correctness by XREAL_0:def 1;
end;

theorem
  for S be non empty finite set,
  s be FinSequence of S, x be set holds
  frequency(x,s)=(len s)* FDprobability (x,s)
  proof
    let S be non empty finite set, s be FinSequence of S,x be set;
    per cases;
    suppose s is non empty;
      hence thesis by XCMPLX_1:88;
    end;
    suppose s is empty; then
      event_pick(x,s)={} by RELAT_1:172;
      then frequency(x,s)=0;
      hence thesis;
    end;
  end;

definition let S be non empty finite set, s be FinSequence of S;
  func FDprobSEQ (s) -> FinSequence of REAL means
  :defFREQDIST:
  dom it= Seg (card (S)) & for n be Nat st n in dom it
  holds it.n=FDprobability((canFS(S)).n,s);
  existence
  proof
    defpred P[Nat,set] means
    $2=FDprobability((canFS(S)).$1,s);
    P0: for k be Nat st k in Seg (card (S))
    ex x being Element of REAL st P[k,x];
    consider g be FinSequence of REAL such that
    P1: dom g =Seg (card (S))
    & for n be Nat st n in Seg (card (S)) holds P[n,g.n]
    from FINSEQ_1:sch 5(P0);
    take g;
    thus thesis by P1;
  end;
  uniqueness
  proof
    let g,h be FinSequence of REAL;
    assume
    A1: dom g =Seg (card (S)) & for n be Nat st n in dom g
    holds g.n=FDprobability((canFS(S)).n,s);
    assume
    A2: dom h =Seg (card (S)) & for n be Nat st n in dom h
    holds h.n=FDprobability((canFS(S)).n,s);
    A6: len g =card (S) by A1,FINSEQ_1:def 3
    .=len h by A2,FINSEQ_1:def 3;
    now let n be Nat;
      assume A6: n in dom g;
      thus g.n = FDprobability((canFS(S)).n,s) by A6,A1
      .= h.n by A6,A1,A2;
    end;
    hence thesis by FINSEQ_2:10,A6;
  end;
end;

theorem
  for S be non empty finite set,
  s be non empty FinSequence of S, x be set holds
  FDprobability(x,s)=prob(event_pick(x,s)) by nazo6;

definition let S be non empty finite set,
  s,t be FinSequence of S;
  pred s,t -are_prob_equivalent means :defequiv:
  for x be set holds FDprobability (x,s)=FDprobability (x,t);
  reflexivity;
  symmetry;
end;

theorem EQX01:
  for S be non empty finite set, s,t,u be FinSequence of S st
  s,t -are_prob_equivalent & t,u -are_prob_equivalent holds
  s,u -are_prob_equivalent
  proof
    let S be non empty finite set;
    let s,t,u be FinSequence of S;
  assume AS1: s,t -are_prob_equivalent & t,u -are_prob_equivalent;
  now let x be set;
    thus FDprobability (x,s)=FDprobability (x,t) by AS1,defequiv
    .=FDprobability (x,u) by AS1,defequiv;
  end;
  hence s,u -are_prob_equivalent by defequiv;
end;

definition let S be non empty finite set, s be FinSequence of S;
  func Finseq-EQclass(s) -> non empty Subset of S* equals
    {t where t is FinSequence of S: s,t -are_prob_equivalent};
  correctness
  proof
    P0P: s in {t where t is FinSequence of S: s,t -are_prob_equivalent};
    {t where t is FinSequence of S: s,t -are_prob_equivalent } c= S*
    proof
      let x be set;
      assume x in {t where t is FinSequence of S : s,t -are_prob_equivalent };
      then ex t be FinSequence of S
      st x=t & s,t -are_prob_equivalent;
      hence x in S* by FINSEQ_1:def 11;
    end;
    hence thesis by P0P;
  end;
end;

theorem EQX02:
  for S be non empty finite set, s,t be FinSequence of S holds
  (s,t -are_prob_equivalent iff t in Finseq-EQclass(s))
  proof
    let S be non empty finite set, s,t be FinSequence of S;
    now assume t in Finseq-EQclass(s); then
      ex t0 be FinSequence of S
      st t=t0 & s,t0 -are_prob_equivalent;
      hence s,t -are_prob_equivalent;
    end;
    hence s,t -are_prob_equivalent iff t in Finseq-EQclass(s);
  end;

theorem EQX03:
  for S be non empty finite set,
  s be FinSequence of S holds s in Finseq-EQclass(s);

theorem EQX04:
  for S be non empty finite set,
  s,t be FinSequence of S holds
  s,t -are_prob_equivalent iff Finseq-EQclass(s) = Finseq-EQclass(t)
  proof
    let S be non empty finite set,
    s,t be FinSequence of S;
    P1: now assume
    P10: s,t -are_prob_equivalent;
    now let x be set;
      assume x in Finseq-EQclass(s); then
      consider u be FinSequence of S such that
      P11: x=u & s,u -are_prob_equivalent;
      t,u -are_prob_equivalent by EQX01,P10,P11;
      hence x in Finseq-EQclass(t) by P11;
    end; then
    P11: Finseq-EQclass(s) c= Finseq-EQclass(t) by TARSKI:def 3;
    now let x be set;
      assume x in Finseq-EQclass(t);
      then consider u be FinSequence of S such that
      P11: x=u & t,u -are_prob_equivalent;
      s,u -are_prob_equivalent by EQX01,P11,P10;
      hence x in Finseq-EQclass(s) by P11;
    end;
    then Finseq-EQclass(t) c= Finseq-EQclass(s) by TARSKI:def 3;
    hence Finseq-EQclass(t) = Finseq-EQclass(s) by XBOOLE_0:def 10,P11;
  end;
  now assume Finseq-EQclass(s) = Finseq-EQclass(t);
    then s in Finseq-EQclass(t);
    hence s,t -are_prob_equivalent by EQX02;
  end;
  hence thesis by P1;
end;

definition
  let S be non empty finite set;
  defpred P[set] means ex u being FinSequence of S st
  $1 = Finseq-EQclass(u);
  func distribution_family(S) -> non empty Subset-Family of S* means
  :defQuot:
  for A being Subset of S* holds
  A in it iff ex s being FinSequence of S st A = Finseq-EQclass(s);
  existence
  proof
    consider T be Subset-Family of S* such that
    P1: for A being Subset of S* holds A in T
    iff P[A] from SUBSET_1:sch 3;
    consider s be Element of S*;
    Finseq-EQclass(s) in T by P1;
    hence thesis by P1;
  end;
  uniqueness
  proof
    let F1,F2 be non empty Subset-Family of S*;
    assume that
    A1: for A being Subset of S* holds A in F1 iff P[A] and
    A2: for A being Subset of S* holds A in F2 iff P[A];
    thus thesis from SUBSET_1:sch 4(A1,A2);
  end;
end;

theorem EQX05:
  for S be non empty finite set,
  s,t be FinSequence of S holds
  s,t -are_prob_equivalent iff FDprobSEQ(s) = FDprobSEQ(t)
  proof
    let S be non empty finite set,
    s,t be FinSequence of S;
    P0: now assume AS: s,t -are_prob_equivalent;
    P1: dom FDprobSEQ (t) = Seg (card (S)) by defFREQDIST;
    now let n be Nat;
      assume P21: n in dom FDprobSEQ (t);
      thus (FDprobSEQ (t)).n
       =FDprobability((canFS(S)).n,t) by P21,defFREQDIST
      .=FDprobability((canFS(S)).n,s) by AS,defequiv;
    end;
    hence FDprobSEQ (s)=FDprobSEQ (t) by P1, defFREQDIST;
  end;
  now assume AS: FDprobSEQ (s) = FDprobSEQ (t);
    for x be set holds FDprobability(x,t) =FDprobability(x,s)
    proof let x be set;
      per cases;
      suppose x in S;
        then x in rng canFS(S) by FUNCT_2:def 3;
        then consider n be set such that
        C11: n in dom (canFS(S)) & x=(canFS(S)).n by FUNCT_1:def 5;
        reconsider n as Element of NAT by C11;
        len canFS(S) = card (S) by UPROOTS:5; then
        C110:n in Seg (card (S)) by C11,FINSEQ_1:def 3; then
        C12: n in dom (FDprobSEQ (s)) by defFREQDIST;
        C13: n in dom (FDprobSEQ (t)) by C110,defFREQDIST;
        thus FDprobability(x,s) = (FDprobSEQ (s)).n by C12,defFREQDIST,C11
        .= FDprobability(x,t) by C11,C13,defFREQDIST,AS;
      end;
      suppose C2: not x in S;
        C21P: s"{x} = {}
        proof
          assume s"{x} <> {}; then
          consider y be set such that
          AA1: y in s"{x} by XBOOLE_0:def 1;
          AA2:y in dom s & s.y in {x} by FUNCT_1:def 13,AA1;
          then s.y in rng s by FUNCT_1:12;
          then s.y in S & s.y=x by AA2,TARSKI:def 1;
          hence contradiction by C2;
        end;
        C22P: t"{x} = {}
        proof
          assume t"{x} <> {};
          then consider y be set such that
          AA1: y in t"{x} by XBOOLE_0:def 1;
          AA2:y in dom t & t.y in {x} by FUNCT_1:def 13,AA1;
          then t.y in rng t by FUNCT_1:12;
          then t.y in S & t.y=x by AA2,TARSKI:def 1;
          hence contradiction by C2;
        end;
        thus FDprobability(x,s)=0 by C21P .=FDprobability(x,t) by C22P;
      end;
    end;
    hence s,t -are_prob_equivalent by defequiv;
  end;
  hence thesis by P0;
end;

theorem
  for S be non empty finite set,
  s,t be FinSequence of S st t in Finseq-EQclass(s)
  holds FDprobSEQ(s)=FDprobSEQ(t)
  proof
    let S be non empty finite set,
    s,t be FinSequence of S;
    assume t in Finseq-EQclass(s);
    then ex w be FinSequence of S
    st t=w & s,w -are_prob_equivalent;
    hence thesis by EQX05;
  end;

definition let S be non empty finite set;
  func GenProbSEQ (S) -> Function of distribution_family(S),REAL* means
  :defFREQDIST2:
  for x be Element of distribution_family(S) holds
  ex s be FinSequence of S st s in x & it.x=FDprobSEQ (s);
  existence
  proof
    defpred P[set,set] means
    ex s be FinSequence of S st s in $1 & $2=FDprobSEQ (s);
    P0: for x being Element of distribution_family(S)
    ex y be Element of REAL* st P[x,y]
    proof
      let x be Element of distribution_family(S);
      reconsider A =x as Subset of S*;
      consider s being FinSequence of S such that
      P02: A = Finseq-EQclass(s) by defQuot;
      FDprobSEQ (s) in REAL* by FINSEQ_1:def 11;
      hence thesis by EQX03,P02;
    end;
    consider g be Function of distribution_family(S), REAL* such that
    P1: for x being Element of distribution_family(S) holds P[x,g.x]
    from FUNCT_2:sch 3(P0);
    take g;
    thus thesis by P1;
  end;
  uniqueness
  proof
    let g,h be Function of distribution_family(S), REAL*;
    assume
    A1: for x be Element of distribution_family(S) holds
    ex s be FinSequence of S st s in x & g.x=FDprobSEQ (s);
    assume
    A2: for x be Element of distribution_family(S) holds
    ex s be FinSequence of S st s in x & h.x=FDprobSEQ (s);
    now let x be Element of distribution_family(S);
      reconsider A =x as Subset of S*;
      consider u being FinSequence of S such that
      P02: A = Finseq-EQclass(u) by defQuot;
      consider s be FinSequence of S such that
      A3: s in x & g.x=FDprobSEQ (s) by A1;
      consider t be FinSequence of S such that
      A4: t in x & h.x=FDprobSEQ (t) by A2;
      A5: u,s -are_prob_equivalent by EQX02,P02,A3;
      t,u -are_prob_equivalent by EQX02,P02,A4;
      then t,s -are_prob_equivalent by A5,EQX01;
      hence g.x = h.x by A3,A4,EQX05;
    end;
    hence thesis by FUNCT_2:def 9;
  end;
end;

theorem EQX07:
  for S be non empty finite set, s be FinSequence of S holds
  (GenProbSEQ (S)).(Finseq-EQclass(s)) = FDprobSEQ (s)
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    Finseq-EQclass(s) is Element of distribution_family(S) by defQuot;
    then consider u be FinSequence of S such that
    P2: u in Finseq-EQclass(s) & (GenProbSEQ (S)).(Finseq-EQclass(s))
    =FDprobSEQ (u) by defFREQDIST2;
    s,u -are_prob_equivalent by P2,EQX02;
    hence thesis by P2,EQX05;
  end;

EQX08: for S be non empty finite set holds GenProbSEQ (S) is one-to-one
  proof
    let S be non empty finite set;
    now let x1,x2 be set;
      assume AS: x1 in distribution_family(S)
      & x2 in distribution_family(S)
      & (GenProbSEQ (S)).x1 =(GenProbSEQ (S)).x2;
      then consider u be FinSequence of S such that
      P2: u in x1 & (GenProbSEQ (S)).x1 =FDprobSEQ (u) by defFREQDIST2;
      consider v be FinSequence of S such that
      P3: v in x2 & (GenProbSEQ (S)).x2 =FDprobSEQ (v) by defFREQDIST2,AS;
      P4: u,v -are_prob_equivalent by EQX05,AS,P2,P3;
      reconsider A1 =x1 as Subset of S* by AS;
      consider u1 being FinSequence of S such that
      P02: A1 = Finseq-EQclass(u1) by defQuot,AS;
      reconsider A2 =x2 as Subset of S* by AS;
      consider u2 being FinSequence of S such that
      P03: A2 = Finseq-EQclass(u2) by defQuot,AS;
      P5: u1,u -are_prob_equivalent by EQX02,P2,P02;
      P6: v,u2 -are_prob_equivalent by EQX02,P3,P03;
      u1,v -are_prob_equivalent by EQX01,P4,P5;
      then u1,u2 -are_prob_equivalent by EQX01,P6;
      hence x1=x2 by P02,P03,EQX04;
    end;
    hence thesis by FUNCT_2:25;
  end;

registration let S be non empty finite set;
  cluster GenProbSEQ S -> one-to-one;
  coherence by EQX08;
end;

definition
  let S be non empty finite set,
  p be ProbFinS FinSequence of REAL;
  assume AS: len p=card S &
  ex s be FinSequence of S st FDprobSEQ (s)=p;
  func distribution( p,S ) -> Element of distribution_family(S) means
  :defBUNBPU:
  (GenProbSEQ S).it = p;
  existence
  proof
    consider s be FinSequence of S such that L1: FDprobSEQ (s)=p by AS;
    consider CS be non empty Subset of S* such that
    L3: CS=Finseq-EQclass(s);
    reconsider CS as Element of distribution_family(S) by defQuot,L3;
    take CS;
    thus thesis by L1,EQX07,L3;
  end;
  uniqueness
  proof
    let CS1,CS2 be Element of distribution_family(S);
    assume U1:(GenProbSEQ (S)).CS1 = p;
    assume U2:(GenProbSEQ (S)).CS2 = p;
    CS1 in dom (GenProbSEQ (S)) &
    CS2 in dom (GenProbSEQ (S)) by FUNCT_1:def 4,U1,U2;
    hence thesis by FUNCT_1:def 8,U1,U2;
  end;
end;

definition let S be non empty finite set,
  s be FinSequence of S;
  func freqSEQ (s) -> FinSequence of NAT means :defDIST:
  dom it= Seg (card S) & for n be Nat st n in dom it
  holds it.n=(len s) * (FDprobSEQ(s)).n;
  existence
  proof
    defpred P[Nat,set ] means $2=(len s) * (FDprobSEQ(s)).$1;
    P0: for k be Nat st k in Seg (card (S))
    ex x being Element of NAT st P[k,x]
    proof
      let k be Nat;
      assume SAS1: k in Seg(card (S));
      then SAS3P:
      k in dom FDprobSEQ(s) by defFREQDIST;
      consider y be Real such that
      SAS4: y =(len s)*(FDprobSEQ(s)).k;
      Seg (len canFS(S))=Seg (card S) by UPROOTS:5; then
      SAS5:k in dom (canFS(S)) by SAS1,FINSEQ_1:def 3;
      rng (canFS(S))= S by FUNCT_2:def 3;
      then (canFS(S)).k is Element of S by SAS5,FUNCT_1:12;
      then consider a be Element of S such that SAS7: a=(canFS(S)).k;
      SAS8:y=(len s)*FDprobability(a,s) by SAS3P,SAS4,SAS7,defFREQDIST;
      SAS9: y is Element of NAT
      proof
        per cases;
          suppose s={};
            hence thesis by SAS8;
          end;
          suppose s<>{};
            hence thesis by SAS8,XCMPLX_1:88;
          end;
      end;
      take y;
      thus thesis by SAS4,SAS9;
    end;
    consider g be FinSequence of NAT such that
    P1: dom g =Seg (card (S))
    & for n be Nat st n in Seg (card (S)) holds P[n,g.n]
    from FINSEQ_1:sch 5(P0);
    take g;
    thus thesis by P1;
  end;
  uniqueness
  proof
    let g,h be FinSequence of NAT;
    assume
    A1: dom g =Seg (card (S)) & for n be Nat st n in dom g
    holds g.n=(len s) * (FDprobSEQ(s)).n;
    assume
    A2: dom h =Seg (card (S)) & for n be Nat st n in dom h
    holds h.n=(len s) * (FDprobSEQ(s)).n;
    A6: len g =card (S) by A1,FINSEQ_1:def 3
    .=len h by A2,FINSEQ_1:def 3;
    now let n be Nat;
      assume A6: n in dom g;
      thus g.n =(len s) * (FDprobSEQ(s)).n by A6,A1
      .= h.n by A6,A1,A2;
    end;
    hence thesis by FINSEQ_2:10,A6;
  end;
end;

theorem nazonazo:
  for S be non empty finite set,
  s be non empty FinSequence of S, n be Nat st n in Seg (card S)
  ex x be Element of S st (freqSEQ(s)).n=frequency(x,s)& x=(canFS(S)).n
  proof
    let S be non empty finite set,
    s be non empty FinSequence of S, n be Nat;
    assume SAS1: n in Seg(card (S));
    SAS2: n in dom freqSEQ(s)
    & n in dom FDprobSEQ(s) by defDIST,defFREQDIST,SAS1;
    consider y be Real such that
    SAS4: y =(len s)*(FDprobSEQ(s)).n;
    Seg (len canFS(S))=Seg (card S) by UPROOTS:5; then
    SAS5:n in dom (canFS(S)) by SAS1,FINSEQ_1:def 3;
    rng (canFS(S))= S by FUNCT_2:def 3;
    then (canFS(S)).n is Element of S by SAS5,FUNCT_1:12;
    then consider a be Element of S such that SAS7: a=(canFS(S)).n;
    SAS8: y=(len s)*FDprobability(a,s) by SAS2,defFREQDIST,SAS4,SAS7;
    T2: y= frequency(a,s) by SAS8,XCMPLX_1:88;
    take a;
    thus thesis by SAS2,T2,SAS7,defDIST,SAS4;
  end;

theorem nnnazo1:
  for S be non empty finite set, s be FinSequence of S holds
  freqSEQ (s) =(len s)* ((FDprobSEQ(s)))
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    P1: dom ((len s) (#) ( (FDprobSEQ(s))))
    =dom (FDprobSEQ(s)) by VALUED_1:def 5
    .=Seg (card (S)) by defFREQDIST
    .= dom (freqSEQ (s)) by defDIST;
    now let m be Nat;
      assume A1: m in dom ((len s) (#) ( (FDprobSEQ(s))));
      hence ((len s) (#) ( (FDprobSEQ(s)))).m
      =(len s)* ( (FDprobSEQ(s))).m by VALUED_1:def 5
      .= (freqSEQ (s)).m by A1,P1,defDIST;
    end;
    hence freqSEQ s = (len s) (#) (FDprobSEQ s) by FINSEQ_1:17,P1;
  end;

theorem nnazo2:
  for S be non empty finite set,
  s be FinSequence of S holds
  Sum ( freqSEQ (s))=(len s)* Sum(FDprobSEQ(s))
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    freqSEQ (s) =(len s)*FDprobSEQ(s) by nnnazo1;
    hence thesis by RVSUM_1:117;
  end;

theorem
  for S be non empty finite set,
  s be non empty FinSequence of S, n be Nat st n in dom s
  ex m be Nat st (freqSEQ(s)).m = frequency(s.n,s) & s.n=(canFS(S)).m
  proof
    let S be non empty finite set,
    s be non empty FinSequence of S,
    n be Nat;
    assume AS: n in dom s;
    set x=s.n;
    x in rng s by FUNCT_1:12,AS;
    then x in S;
    then x in rng (canFS S) by FUNCT_2:def 3;
    then consider m be set such that
    DM: m in dom (canFS(S))& x=(canFS(S)).m by FUNCT_1:def 5;
    reconsider m as Nat by DM;
    Seg len (canFS(S))= Seg (card (S)) by UPROOTS:5;
    then J1P: dom (canFS(S))=Seg(card (S)) by FINSEQ_1:def 3;
    consider xx be Element of S such that J2: (freqSEQ(s)).m
    =frequency(xx,s)& xx=(canFS(S)).m by nazonazo,J1P,DM;
    take m;
    thus thesis by DM,J2;
  end;

theorem LMCARD1:
  for n be Nat, S be Function,L be FinSequence of NAT
  st S is disjoint_valued & dom S = dom L & n=len L
  & for i be Nat st i in dom S holds
  S.i is finite & L.i = card (S.i)
  holds union rng S is finite &
  card (union rng S) = Sum L
  proof
    defpred P[Nat] means
    for S be Function,L be FinSequence of NAT
    st S is disjoint_valued & dom S = dom L & $1=len L
    & for i be Nat st i in dom S holds
    S.i is finite & L.i = card (S.i) holds
    union rng S is finite & card (union rng S ) = Sum L;
    P0: P[0]
    proof
      let S be Function,L be FinSequence of NAT;
      assume AS0:
      S is disjoint_valued & dom S = dom L & 0=len L
      & for i be Nat st i in dom S holds
      S.i is finite & L.i = card (S.i);
      P0: L= {} by AS0;
      then S= {} by AS0;
      then for X be set st X in rng S holds X c= {}; then
      P3P: union rng S c= {} by ZFMISC_1:94;
      thus union rng S is finite &
      card (union rng S) = Sum L by P3P,P0,RVSUM_1:102;
    end;
    PN: now let n be Nat;
    assume P1: P[n];
    now let S be Function,L be FinSequence of NAT;
      assume
      ASN: S is disjoint_valued & dom S = dom L & (n+1)=len L
      & for i be Nat st i in dom S holds
      S.i is finite & L.i = card (S.i);
      reconsider SN=S|(Seg n) as Function;
      reconsider LN=L|n as FinSequence of NAT;
      n+1 in Seg (len L) by ASN,FINSEQ_1:6; then
      Q0: n+1 in dom S by ASN,FINSEQ_1:def 3;
      Q1:SN is disjoint_valued
      proof
        now let x,y be set;
          assume
          A1: x <> y;
          per cases;
            suppose x in dom SN & y in dom SN;
              then SN.x=S.x & SN.y= S.y by FUNCT_1:70;
              hence SN.x misses SN.y by A1,ASN,PROB_2:def 3;
            end;
            suppose A12: not (x in dom SN & y in dom SN );
              now per cases by A12;
                suppose not x in dom SN;
                  then SN.x= {} by FUNCT_1:def 4;
                  then SN.x /\ SN.y = {};
                  hence SN.x misses SN.y by XBOOLE_0:def 7;
                end;
                suppose not y in dom SN;
                  then SN.y= {} by FUNCT_1:def 4;
                  then SN.x /\ SN.y = {};
                  hence SN.x misses SN.y by XBOOLE_0:def 7;
                end;
              end;
              hence SN.x misses SN.y;
            end;
        end;
        hence thesis by PROB_2:def 3;
      end;
      Q2:dom SN = dom S /\ Seg n by RELAT_1:90
      .= dom LN by RELAT_1:90,ASN;
      Q3:n=len LN by FINSEQ_1:80,ASN,NAT_1:12;
      Q4:for i be Nat st i in dom SN holds
      SN.i is finite & LN.i = card (SN.i)
      proof
        let i be Nat;
        assume A2P:i in dom SN; then
        A2:i in dom S /\ Seg n by RELAT_1:90; then
        A3:i in dom S & i in Seg n by XBOOLE_0:def 4;
        LN.i = L.i by FUNCT_1:71,ASN,A2
        .= card (S.i) by ASN,A3
        .= card (SN.i) by A2P,FUNCT_1:70;
        hence thesis;
      end;
      Q5:union rng SN is finite &
      card (union rng SN ) = Sum LN by P1,Q1,Q2,Q3,Q4;
      Q6: (union rng SN) \/ S.(n+1) = (union rng S)
      proof
        now let x be set;
          assume x in (union rng S);
          then consider y be set such that
          A9: x in y & y in rng S by TARSKI:def 4;
          consider i be set such that
          A3: i in dom S & y=S.i by A9,FUNCT_1:def 5;
          A4:i in Seg (n+1) by ASN,FINSEQ_1:def 3,A3;
          reconsider i as Element of NAT by ASN,A3;
          A5: 1<=i & i <= n+1 by FINSEQ_1:3,A4;
          now per cases;
            suppose i=n+1;
              hence x in (union rng SN) \/ S.(n+1) by XBOOLE_0:def 3,A3,A9;
            end;
            suppose i<> n+1;
              then i < n+1 by A5,XXREAL_0:1;
              then i <= n by NAT_1:13;
              then i in Seg n by A5;
              then i in dom S /\ Seg n by A3,XBOOLE_0:def 4;
              then
              A8: i in dom SN by RELAT_1:90;
              then S.i = SN.i by FUNCT_1:70;
              then y in rng SN by FUNCT_1:def 5,A3,A8;
              then x in (union rng SN) by A9,TARSKI:def 4;
              hence x in (union rng SN) \/ S.(n+1) by XBOOLE_0:def 3;
            end;
          end;
          hence x in (union rng SN) \/ S.(n+1);
        end;
        then
        L1: (union rng S) c= (union rng SN) \/ S.(n+1) by TARSKI:def 3;
        (union rng SN) \/ S.(n+1) c= (union rng S)
        proof
          let x be set;
          assume A3P: x in (union rng SN) \/ S.(n+1);
          now per cases by A3P,XBOOLE_0:def 3;
            suppose C1: x in S.(n+1);
              n+1 in Seg (n+1) by FINSEQ_1:6;
              then n+1 in dom S by ASN,FINSEQ_1:def 3;
              then S.(n+1) in rng S by FUNCT_1:def 5;
              hence x in union rng S by C1,TARSKI:def 4;
            end;
            suppose x in (union rng SN);
              then consider y be set such that
              A9: x in y & y in rng SN by TARSKI:def 4;
              consider i be set such that
              A3: i in dom SN & y=SN.i by A9,FUNCT_1:def 5;
              A4: i in dom S /\ Seg n by RELAT_1:90,A3;
              A5: SN.i = S.i by FUNCT_1:70,A3;
              i in dom S by A4,XBOOLE_0:def 4;
              then y in rng S by A3,A5,FUNCT_1:def 5;
              hence x in (union rng S) by A9,TARSKI:def 4;
            end;
          end;
          hence x in (union rng S);
        end;
        hence thesis by L1,XBOOLE_0:def 10;
      end;
      AA: 1<= (n+1) & n+1 <= len L by ASN,NAT_1:11;
      Q7P:L= (L|n)^ <* L/.len L *> by ASN,FINSEQ_5:24
      .=LN^<*L.(n+1)*> by AA,ASN,FINSEQ_4:24;
      reconsider USN= union rng SN as finite set by P1,Q1,Q2,Q3,Q4;
      reconsider S1= S.(n+1) as finite set by ASN,Q0;
      union rng S = USN \/ S1 by Q6;
      hence (union rng S) is finite;
      for z be set st z in rng SN holds z misses S.(n+1)
      proof
        let y be set;
        assume
        A2: y in rng SN;
        consider i be set such that
        A3: i in dom SN & y=SN.i by A2,FUNCT_1:def 5;
        A4P: i in dom S /\ Seg n by A3,RELAT_1:90; then
        A4:i in Seg n by XBOOLE_0:def 4;
        reconsider i as Element of NAT by A4P;
        i <= n by FINSEQ_1:3,A4; then
        A0P: i <> n+1 by NAT_1:13;
        y=S.i by A3,FUNCT_1:70;
        hence thesis by A0P,PROB_2:def 3,ASN;
      end;
      then
      Q9: union rng SN misses S.(n+1) by ZFMISC_1:98;
      Q8: card ((union rng SN) \/ S.(n+1) )
      =card (USN)+ card (S1) by Q9,CARD_2:53;
      thus card (union rng S ) = Sum LN + L.(n+1) by Q5,ASN,Q0,Q8,Q6
      .= Sum L by Q7P,RVSUM_1:104;
    end;
    hence P[n+1];
  end;
  thus for n be Nat holds P[n] from NAT_1:sch 2(P0,PN);
end;

theorem LMCARD:
  for S be Function,L be FinSequence of NAT
  st S is disjoint_valued & dom S = dom L
  & for i be Nat st i in dom S holds
  S.i is finite & L.i = card (S.i)
  holds union rng S is finite
  & card (union rng S ) = Sum L
  proof
    let S be Function,L be FinSequence of NAT;
    assume AS: S is disjoint_valued & dom S = dom L
    & for i be Nat st i in dom S holds
    S.i is finite & L.i = card (S.i);
    len L is Element of NAT;
    hence thesis by LMCARD1,AS;
  end;

theorem DISTSUM:
  for S be non empty finite set,
  s be non empty FinSequence of S holds
  Sum freqSEQ (s) = len s
  proof
    let S be non empty finite set,
    s be non empty FinSequence of S;
    set L= freqSEQ (s);
    defpred P[set,set] means ex z be Element of S
    st z=(canFS(S)).$1 & $2 = event_pick(z,s);
    len (canFS(S))= card (S) by UPROOTS:5;
    then PP0: dom (canFS(S))=Seg(card (S)) by FINSEQ_1:def 3;
    PP1: for x,y1,y2 be set
    st x in dom L & P[x,y1] & P[x,y2] holds y1 = y2;
    PP2: for x be set st x in dom L ex y be set st P[x,y]
    proof
      let x be set;
      assume x in dom L;
      then LPP22P:x in Seg (card (S)) by defDIST;
      set z= (canFS(S)).x;
      rng (canFS(S))=S by FUNCT_2:def 3;
      then reconsider z as Element of S by FUNCT_1:12,LPP22P,PP0;
      consider y be set such that
      LPP25: y=s"{z};
      LPP26: y=event_pick(z,s) by LPP25;
      take y;
      thus thesis by LPP26;
    end;
    consider T be Function such that
    P1:dom T = dom L &
    for x be set st x in dom L holds P[x,T.x] from FUNCT_1:sch 2(PP1,PP2);
    LMISS1: for a,b be set st
    a in dom T & b in dom T & a<>b holds
    T.a misses T.b
    proof
      let a,b be set;
      assume ZTA: a in dom T & b in dom T & a<>b;
      ZT1: a in dom(canFS(S)) & b in dom(canFS(S)) by P1,ZTA,PP0,defDIST;
      ZT2:(canFS(S)).a<>(canFS(S)).b by ZTA,FUNCT_1:def 8,ZT1;
      consider za be Element of S such that ZT3: za=(canFS(S)).a &
      T.a=event_pick(za,s) by P1,ZTA;
      consider zb be Element of S such that ZT4: zb=(canFS(S)).b &
      T.b=event_pick(zb,s) by P1,ZTA;
      thus thesis by ZT3,ZT4,FUNCT_1:141,ZFMISC_1:17,ZT2;
    end;
    for a,b be set st a<>b holds T.a misses T.b
    proof
      let a,b be set;
      assume ANB: a<>b;
      now per cases;
        case a in dom T & b in dom T;
          hence thesis by LMISS1,ANB;
        end;
        case not a in dom T;
          then T.a={} by FUNCT_1:def 4;
          hence thesis by XBOOLE_1:65;
        end;
        case a in dom T & not b in dom T;
          then T.b={} by FUNCT_1:def 4;
          hence thesis by XBOOLE_1:65;
        end;
      end;
      hence thesis;
    end; then
    Q1: T is disjoint_valued by PROB_2:def 3;
    Q3: for i be Nat st i in dom T holds
    T.i is finite & L.i = card (T.i)
    proof
      let i be Nat;
      assume ASQ3: i in dom T;
      then consider zi be Element of S such that Q3C1: zi=(canFS(S)).i &
      T.i=event_pick(zi,s) by P1;
      Q3C3:dom L= Seg (card (S)) by defDIST;
      Q3C4:i in dom (FDprobSEQ(s)) by P1,ASQ3,Q3C3,defFREQDIST;
      L.i =(len s) * (FDprobSEQ(s)).i by defDIST,ASQ3,P1
      .=(len s)*FDprobability((canFS(S)).i,s) by Q3C4,defFREQDIST
      .= card (T.i) by Q3C1,XCMPLX_1:88;
      hence thesis;
    end;
    reconsider T1=union rng T as finite set by Q1,P1,Q3,LMCARD;
    for X be set st X in rng T holds X c= Seg (len s)
    proof
      let X be set;
      assume X in rng T;
      then consider j be set such that
      RNGT1: j in dom T & X =T.j by FUNCT_1:def 5;
      consider zj be Element of S such that
      RNGT2: zj=(canFS(S)).j & T.j = event_pick(zj,s) by P1,RNGT1;
      X c= whole_event(s) by RNGT1,RNGT2;
      hence thesis by FINSEQ_1:def 3;
    end; then
    L1: union rng T c= Seg (len s) by ZFMISC_1:94;
    Seg (len s) c=union rng T
    proof
      assume CNTRSEGLS: not Seg (len s) c=union rng T;
      consider ne be set such that SEGLS1:
      ne in Seg (len s) & not ne in union rng T by TARSKI:def 3,CNTRSEGLS;
      SEGLS2: ne in dom s by SEGLS1,FINSEQ_1:def 3;
      set yne=s.ne;
      SEGLS4: yne in rng s by SEGLS2,FUNCT_1:def 5;
      reconsider yne as Element of S by SEGLS4;
      rng (canFS(S))=S by FUNCT_2:def 3;
      then consider nne be set such that
      SEGLS6: nne in dom(canFS(S))&
      yne=(canFS(S)).nne by FUNCT_1:def 5;
      NINDOML:nne in dom L by defDIST,PP0,SEGLS6;
      then consider zne be Element of S such that
      SEGLS7: zne=(canFS(S)).nne &
      T.nne = event_pick(zne,s) by P1;
      s.ne in {s.ne} by TARSKI:def 1;
      then SEGLS9: ne in T.nne by SEGLS7,SEGLS6,FUNCT_1:def 13,SEGLS2;
      T.nne in rng T by FUNCT_1:12,NINDOML,P1;
      hence contradiction by SEGLS1,TARSKI:def 4,SEGLS9;
    end;
    then
    Q5: T1 = Seg (len s) by L1,XBOOLE_0:def 10;
    thus Sum freqSEQ (s) = card (T1) by Q1,P1,Q3,LMCARD
    .= len s by FINSEQ_1:78,Q5;
  end;

theorem FREQDISTSUM:
  for S be non empty finite set,
  s be non empty FinSequence of S holds Sum FDprobSEQ (s) = 1
  proof
    let S be non empty finite set,
    s be non empty FinSequence of S;
    Sum freqSEQ(s) = len s by DISTSUM;
    then (len s)* Sum( (FDprobSEQ(s))) = (len s)*1 by nnazo2;
    hence thesis by XCMPLX_1:5;
  end;

theorem FREQDISTSUM2:
  for S be non empty finite set,
  s be non empty FinSequence of S holds FDprobSEQ (s) is ProbFinS
  proof
    let S be non empty finite set,
    s be non empty FinSequence of S;
    L0: Sum FDprobSEQ (s) = 1 by FREQDISTSUM;
    for i be Element of NAT st i in dom (FDprobSEQ(s))
    holds (FDprobSEQ(s)).i>=0
    proof
      let i be Element of NAT;
      assume CAS: i in dom (FDprobSEQ(s));
      (FDprobSEQ(s)).i =FDprobability((canFS(S)).i,s) by CAS,defFREQDIST;
      hence thesis;
    end;
    hence thesis by L0,MATRPROB:def 5;
  end;

definition
  let S be non empty finite set;
  mode distProbFinS of S -> ProbFinS FinSequence of REAL means
  :defdistProbFinS:
  len it=card S & ex s be FinSequence of S st FDprobSEQ (s)=it;
  existence
  proof
    consider a be Element of S;
    set s=<*a*>;
    reconsider p=FDprobSEQ (s) as ProbFinS FinSequence of REAL
    by FREQDISTSUM2;
    dom p= Seg (card (S)) by defFREQDIST;
    then len (p) =card S by FINSEQ_1:def 3;
    hence thesis;
  end;
end;

theorem pbf:
  for S be non empty finite set,
  p be distProbFinS of S holds
  p is ProbFinS FinSequence of REAL
  & len p=card S & (ex s be FinSequence of S st FDprobSEQ (s)=p)
  & distribution( p,S ) is Element of distribution_family(S)
  & (GenProbSEQ (S)).distribution( p,S ) = p
  proof
    let S be non empty finite set,
    p be distProbFinS of S;
    thus p is ProbFinS FinSequence of REAL;
    thus P1: len p=card S & (ex s be FinSequence of S st FDprobSEQ (s)=p)
    by defdistProbFinS;
    thus distribution(p,S) is Element of distribution_family(S);
    thus (GenProbSEQ S).distribution(p,S) = p by defBUNBPU,P1;
  end;

begin :: uniform distribution

definition let S be non empty finite set, s be FinSequence of S;
  pred s is_uniformly_distributed means
  :defunidistseq:
  for n be Nat st n in dom FDprobSEQ (s) holds
  (FDprobSEQ (s)).n=1/(card S);
end;

theorem THUDEQ0:
  for S be non empty finite set,
  s be FinSequence of S st s is_uniformly_distributed
  holds FDprobSEQ (s) is constant
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    assume AS: s is_uniformly_distributed;
    let a,b be set;
    assume a: a in dom FDprobSEQ(s) & b in dom FDprobSEQ(s);
    then reconsider na=a,nb=b as Nat;
    (FDprobSEQ (s)).na = 1/card S by a,AS,defunidistseq
    .= (FDprobSEQ (s)).nb by a,AS,defunidistseq;
    hence thesis;
  end;

theorem THUDEQ:
  for S be non empty finite set,
  s,t be FinSequence of S
  st s is_uniformly_distributed &
  s,t -are_prob_equivalent holds
  t is_uniformly_distributed
  proof
    let S be non empty finite set,
    s,t be FinSequence of S;
    assume AS:s is_uniformly_distributed & s,t -are_prob_equivalent; then
    L1: FDprobSEQ (s)=FDprobSEQ (t) by EQX05;
    for n be Nat st n in dom FDprobSEQ (t) holds
    (FDprobSEQ (t)).n=1/(card S) by L1,AS,defunidistseq;
    hence thesis by defunidistseq;
  end;

theorem THUDEQ2:
  for S be non empty finite set,
  s,t be FinSequence of S st s is_uniformly_distributed &
  t is_uniformly_distributed holds
  s,t -are_prob_equivalent
  proof
    let S be non empty finite set,
    s,t be FinSequence of S;
    assume AS:s is_uniformly_distributed &
    t is_uniformly_distributed;
    L1: dom FDprobSEQ (s)= Seg (card (S)) &
    dom FDprobSEQ (t)= Seg (card (S)) by defFREQDIST;
    for n be set st n in dom FDprobSEQ (s) holds
    (FDprobSEQ (s)).n=(FDprobSEQ (t)).n
    proof
      let n be set;
      assume n in dom FDprobSEQ (s); then
      (FDprobSEQ (s)).n= 1/(card S)
      &(FDprobSEQ (t)).n= 1/(card S) by defunidistseq,AS,L1;
      hence thesis;
    end;
    then FDprobSEQ (s) = FDprobSEQ (t) by L1,FUNCT_1:9;
    hence thesis by EQX05;
  end;

theorem THUDS:
  for S be non empty finite set holds
  canFS(S) is_uniformly_distributed
  proof
    let S be non empty finite set;
    set s = canFS(S);
    L0: len s= card S by UPROOTS:5;then
    dom s= Seg(card S) by FINSEQ_1:def 3;
    then L01: dom s=dom FDprobSEQ (s) by defFREQDIST;
    for n be Nat st n in dom s
    holds (FDprobSEQ (s)).n=1/(card S)
    proof
      let n be Nat;
      assume ASB: n in dom s; then
      (FDprobSEQ (s)).n=FDprobability(s.n,s) by defFREQDIST,L01
      .= card ({n}) /(len s) by FINSEQ_5:4,ASB
      .= 1/(card S) by L0,CARD_1:50;
      hence thesis;
    end;
    hence thesis by defunidistseq,L01;
  end;

  THCFS:
  for S be non empty finite set,
  s be FinSequence of S st s in Finseq-EQclass(canFS(S)) holds
  s is_uniformly_distributed
  proof
    let S be non empty finite set, s be FinSequence of S;
    consider CS be non empty Subset of S*
    such that L3: CS=Finseq-EQclass(canFS(S));
    reconsider CS as Element of distribution_family(S) by defQuot,L3;
    assume s in Finseq-EQclass(canFS(S)); then
    s,canFS(S) -are_prob_equivalent by EQX02;
    hence thesis by THUDEQ,THUDS;
  end;

  THCFS2:
  for S be non empty finite set,
  s be FinSequence of S
  st s is_uniformly_distributed holds
  for t be FinSequence of S st
  t is_uniformly_distributed holds
  t in Finseq-EQclass(s)
  proof
    let S be non empty finite set,
    s be FinSequence of S;
    assume L1: s is_uniformly_distributed;
    for t be FinSequence of S st t is_uniformly_distributed holds
    t in Finseq-EQclass(s)
    proof
      let t be FinSequence of S;
      assume t is_uniformly_distributed;
      then s,t -are_prob_equivalent by L1,THUDEQ2;
      hence thesis;
    end;
    hence thesis;
  end;

definition let S be non empty finite set;
  func uniform_distribution(S) -> Element of distribution_family(S) means
  :defunidist:
  for s be FinSequence of S holds s in it iff s is_uniformly_distributed;
  existence
  proof
    consider s be FinSequence of S such that L1: s=canFS(S);
    L2: s is_uniformly_distributed by L1,THUDS;
    consider CS be non empty Subset of S*
    such that L3: CS=Finseq-EQclass(s);
    reconsider CS as Element of distribution_family(S) by defQuot,L3;
    for t be FinSequence of S
    st t in CS holds
    s,t -are_prob_equivalent by EQX02,L3; then
    L5: for t be FinSequence of S
    st t in CS holds t is_uniformly_distributed by L2,THUDEQ;
    take CS;
    thus thesis by L2,L5,THCFS2,L3;
  end;
  uniqueness
  proof
    let A,B be Element of distribution_family(S);
    assume U1:
    for s be FinSequence of S holds s in A iff s is_uniformly_distributed;
    assume U2:
    for s be FinSequence of S holds s in B iff s is_uniformly_distributed;
    N1: for s be set st s in A holds s in B
    proof
      let s be set;
      assume A1:s in A;
      then reconsider s as Element of S*;
      s is_uniformly_distributed by U1,A1;
      hence thesis by U2;
    end;
    for s be set st s in B holds s in A
    proof
      let s be set;
      assume A1: s in B;
      then reconsider s as Element of S*;
      s is_uniformly_distributed by U2,A1;
      hence thesis by U1;
    end;
    hence thesis by N1,TARSKI:2;
  end;
end;

registration
  let S be non empty finite set;
  cluster constant distProbFinS of S;
  existence
  proof
    consider s be FinSequence of S such that L1: s=canFS(S);
    reconsider s as Element of S* by FINSEQ_1:def 11;
    consider p be FinSequence of REAL
    such that L3: p= FDprobSEQ (s);
    T1: p is constant by THUDEQ0,L3,L1,THUDS;
    T2: p is ProbFinS by L1,FREQDISTSUM2,L3;
    T3: dom p= Seg (card (S)) by defFREQDIST,L3;
    T4:len p=card S by T3,FINSEQ_1:def 3;
    take p;
    thus thesis by T1,defdistProbFinS,L3,T2,T4;
  end;
end;

definition
  let S be non empty finite set;
  func Uniform_FDprobSEQ(S) -> constant distProbFinS of S equals
    FDprobSEQ (canFS(S));
  coherence
  proof
    set s=canFS(S);
    reconsider s as Element of S* by FINSEQ_1:def 11;
    consider p be FinSequence of REAL such that L3:p= FDprobSEQ (s);
    L4: p is constant by THUDEQ0,L3,THUDS;
    T2: p is ProbFinS by FREQDISTSUM2,L3;
    T3: dom p= Seg (card (S)) by defFREQDIST,L3;
    len p=card (S) by T3,FINSEQ_1:def 3;
    hence thesis by defdistProbFinS,L3,T2,L4;
  end;
end;

theorem
  for S be non empty finite set holds
  uniform_distribution(S)=distribution(Uniform_FDprobSEQ(S),S)
  proof
    let S be non empty finite set;
    set p=Uniform_FDprobSEQ(S),s=canFS(S);
    ES1:s is_uniformly_distributed by THUDS;
    ZZ0: (GenProbSEQ (S)).(Finseq-EQclass(s)) = p by EQX07;
    ZZ1:for t be FinSequence of S st
    t in Finseq-EQclass(s) holds
    t is_uniformly_distributed by THCFS;
    nazo:Finseq-EQclass(s) is
    Element of distribution_family(S) by defQuot;
    for t be FinSequence of S st
    t is_uniformly_distributed holds t in Finseq-EQclass(s)
    proof
      let t be FinSequence of S;
      assume t is_uniformly_distributed;
      then s,t -are_prob_equivalent by THUDEQ2,ES1;
      hence thesis;
    end;
    then T1: Finseq-EQclass(s)=uniform_distribution(S)
    by ZZ1,defunidist,nazo;
    ZZ02:(GenProbSEQ (S)).distribution( p,S ) =
    (GenProbSEQ (S)).(Finseq-EQclass(s)) by ZZ0,pbf;
    dom (GenProbSEQ (S)) = distribution_family(S) by FUNCT_2:def 1;
    hence thesis by ZZ02,T1,FUNCT_1:def 8;
  end;