:: DIST_1 semantic presentation

begin

notation
let S be set ;
let s be FinSequence of S;
synonym  whole_event s for  dom S;
end;

theorem Th1: :: DIST_1:1
for S being set
for s being FinSequence of S holds whole_event = s " S
proof
let S be set ; ::_thesis: for s being FinSequence of S holds whole_event = s " S
let s be FinSequence of S; ::_thesis: whole_event = s " S
 ( s " S c= s " (rng s) & s " (rng s) c= s " S ) by RELAT_1:135, RELAT_1:143;
then  s " (rng s) = s " S by XBOOLE_0:def_10;
hence  whole_event = s " S by RELAT_1:134; ::_thesis: verum
end;

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

definition
let S be set ;
let s be FinSequence of S;
let x be set ;
:: original: event_pick
redefine func event_pick (x,s) ->  Event of (whole_event );
correctness
coherence
event_pick (,x) is Event of (whole_event );
by RELAT_1:132;
end;

definition
let S be finite set ;
let s be FinSequence of S;
let x be set ;
func frequency (x,s) ->  Nat equals :: DIST_1:def 1
 card (event_pick (x,s));
correctness
coherence
card (event_pick (x,s)) is Nat;
;
end;

:: deftheorem  defines frequency DIST_1:def_1_:_
 for S being finite set
for s being FinSequence of S
for x being set holds frequency (x,s) = card (event_pick (x,s));

theorem :: DIST_1:2
for S being set
for s being FinSequence of S
for e being set st e in whole_event holds
ex x being Element of S st e in event_pick (x,s)
proof
let S be set ; ::_thesis: for s being FinSequence of S
for e being set st e in whole_event holds
ex x being Element of S st e in event_pick (x,s)
let s be FinSequence of S; ::_thesis: for e being set st e in whole_event holds
ex x being Element of S st e in event_pick (x,s)
let e be set ; ::_thesis: ( e in whole_event implies ex x being Element of S st e in event_pick (x,s) )
assume A1: e in whole_event ; ::_thesis: ex x being Element of S st e in event_pick (x,s)
then  e in s " S by Th1;
then  s . e in S by FUNCT_1:def_7;
then consider x being Element of S such that
A2: x = s . e ;
take  x ; ::_thesis: e in event_pick (x,s)
 x in {x} by TARSKI:def_1;
hence  e in event_pick (x,s) by A1, A2, FUNCT_1:def_7; ::_thesis: verum
end;

theorem Th3: :: DIST_1:3
for S being set
for s being FinSequence of S holds card (whole_event ) = len s
proof
let S be set ; ::_thesis: for s being FinSequence of S holds card (whole_event ) = len s
let s be FinSequence of S; ::_thesis: card (whole_event ) = len s
thus  card (whole_event ) = card (Seg (len s)) by FINSEQ_1:def_3
.= len s by FINSEQ_1:57 ; ::_thesis: verum
end;

definition
let S be finite set ;
let s be FinSequence of S;
let x be set ;
func FDprobability (x,s) ->  Real equals :: DIST_1:def 2
(frequency (x,s)) / (len s);
correctness
coherence
(frequency (x,s)) / (len s) is Real;
;
end;

:: deftheorem  defines FDprobability DIST_1:def_2_:_
 for S being finite set
for s being FinSequence of S
for x being set holds FDprobability (x,s) = (frequency (x,s)) / (len s);

theorem :: DIST_1:4
for S being finite set
for s being FinSequence of S
for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))
proof
let S be finite set ; ::_thesis: for s being FinSequence of S
for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))
let s be FinSequence of S; ::_thesis: for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))
let x be set ; ::_thesis: frequency (x,s) = (len s) * (FDprobability (x,s))
percases ( not s is empty or s is empty ) ;
suppose not s is empty ; ::_thesis: frequency (x,s) = (len s) * (FDprobability (x,s))
hence  frequency (x,s) = (len s) * (FDprobability (x,s)) by XCMPLX_1:87; ::_thesis: verum
end;
suppose s is empty ; ::_thesis: frequency (x,s) = (len s) * (FDprobability (x,s))
then  frequency (x,s) = 0 ;
hence  frequency (x,s) = (len s) * (FDprobability (x,s)) ; ::_thesis: verum
end;
end;
end;

definition
let S be finite set ;
let s be FinSequence of S;
func FDprobSEQ s ->  FinSequence of REAL  means :Def3: :: DIST_1:def 3
( dom it = Seg (card S) & ( for n being Nat st n in dom it holds
it . n = FDprobability (((canFS S) . n),s) ) );
existence
 ex b1 being FinSequence of REAL st
( dom b1 = Seg (card S) & ( for n being Nat st n in dom b1 holds
b1 . n = FDprobability (((canFS S) . n),s) ) )
proof
defpred S1[ Nat, set ] means $2 = FDprobability (((canFS S) . $1),s);
A1: for k being Nat st k in Seg (card S) holds
ex x being Element of REAL st S1[k,x] ;
consider g being FinSequence of REAL  such that
A2: ( dom g = Seg (card S) & ( for n being Nat st n in Seg (card S) holds
S1[n,g . n] ) ) from FINSEQ_1:sch_5(A1);
take  g ; ::_thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = FDprobability (((canFS S) . n),s) ) )
thus  ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = FDprobability (((canFS S) . n),s) ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of REAL st dom b1 = Seg (card S) & ( for n being Nat st n in dom b1 holds
b1 . n = FDprobability (((canFS S) . n),s) ) & dom b2 = Seg (card S) & ( for n being Nat st n in dom b2 holds
b2 . n = FDprobability (((canFS S) . n),s) ) holds
b1 = b2
proof
let g, h be FinSequence of REAL ; ::_thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = FDprobability (((canFS S) . n),s) ) & dom h = Seg (card S) & ( for n being Nat st n in dom h holds
h . n = FDprobability (((canFS S) . n),s) ) implies g = h )
assume that
A3: dom g = Seg (card S) and
A4: for n being Nat st n in dom g holds
g . n = FDprobability (((canFS S) . n),s) ; ::_thesis: ( not dom h = Seg (card S) or ex n being Nat st
( n in dom h & not h . n = FDprobability (((canFS S) . n),s) ) or g = h )
assume that
A5: dom h = Seg (card S) and
A6: for n being Nat st n in dom h holds
h . n = FDprobability (((canFS S) . n),s) ; ::_thesis: g = h
A7: now__::_thesis:_for_n_being_Nat_st_n_in_dom_g_holds_
g_._n_=_h_._n
let n be Nat; ::_thesis: ( n in dom g implies g . n = h . n )
assume A8: n in dom g ; ::_thesis: g . n = h . n
hence g . n = FDprobability (((canFS S) . n),s) by A4
.= h . n by A3, A5, A6, A8 ;
::_thesis: verum
end;
len g = card S by A3, FINSEQ_1:def_3
.= len h by A5, FINSEQ_1:def_3 ;
hence  g = h by A7, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines FDprobSEQ DIST_1:def_3_:_
 for S being finite set
for s being FinSequence of S
for b3 being FinSequence of REAL holds
( b3 = FDprobSEQ s iff ( dom b3 = Seg (card S) & ( for n being Nat st n in dom b3 holds
b3 . n = FDprobability (((canFS S) . n),s) ) ) );

theorem :: DIST_1:5
for S being finite set
for s being FinSequence of S
for x being set holds FDprobability (x,s) = prob (event_pick (x,s)) by Th3;

definition
let S be finite set ;
let s, t be FinSequence of S;
preds,t -are_prob_equivalent  means :Def4: :: DIST_1:def 4
 for x being set holds FDprobability (x,s) = FDprobability (x,t);
reflexivity
 for s being FinSequence of S
for x being set holds FDprobability (x,s) = FDprobability (x,s) ;
symmetry
 for s, t being FinSequence of S st ( for x being set holds FDprobability (x,s) = FDprobability (x,t) ) holds
for x being set holds FDprobability (x,t) = FDprobability (x,s) ;
end;

:: deftheorem Def4 defines -are_prob_equivalent DIST_1:def_4_:_
 for S being finite set
for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff for x being set holds FDprobability (x,s) = FDprobability (x,t) );

theorem Th6: :: DIST_1:6
for S being finite set
for s, t, u being FinSequence of S st s,t -are_prob_equivalent & t,u -are_prob_equivalent holds
s,u -are_prob_equivalent
proof
let S be finite set ; ::_thesis: for s, t, u being FinSequence of S st s,t -are_prob_equivalent & t,u -are_prob_equivalent holds
s,u -are_prob_equivalent
let s, t, u be FinSequence of S; ::_thesis: ( s,t -are_prob_equivalent & t,u -are_prob_equivalent implies s,u -are_prob_equivalent )
assume that
A1: s,t -are_prob_equivalent and
A2: t,u -are_prob_equivalent ; ::_thesis: s,u -are_prob_equivalent
let x be set ; :: according to DIST_1:def_4 ::_thesis: FDprobability (x,s) = FDprobability (x,u)
thus  FDprobability (x,s) = FDprobability (x,t) by A1, Def4
.= FDprobability (x,u) by A2, Def4 ; ::_thesis: verum
end;

definition
let S be finite set ;
let s be FinSequence of S;
func Finseq-EQclass s ->  Subset of (S *) equals :: DIST_1:def 5
 {  t where t is FinSequence of S : s,t -are_prob_equivalent  }  ;
correctness
coherence
{  t where t is FinSequence of S : s,t -are_prob_equivalent  }  is Subset of (S *);
proof
  {  t where t is FinSequence of S : s,t -are_prob_equivalent  }  c= S *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  t where t is FinSequence of S : s,t -are_prob_equivalent  }  or x in S * )
assume  x in  {  t where t is FinSequence of S : s,t -are_prob_equivalent  }  ; ::_thesis: x in S *
then  ex t being FinSequence of S st
( x = t & s,t -are_prob_equivalent ) ;
hence  x in S * by FINSEQ_1:def_11; ::_thesis: verum
end;
hence   {  t where t is FinSequence of S : s,t -are_prob_equivalent  }  is Subset of (S *) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Finseq-EQclass DIST_1:def_5_:_
 for S being finite set
for s being FinSequence of S holds Finseq-EQclass s =  {  t where t is FinSequence of S : s,t -are_prob_equivalent  }  ;

registration
let S be finite set ;
let s be FinSequence of S;
cluster Finseq-EQclass s ->  non empty ;
coherence
 not Finseq-EQclass s is empty
proof
 s in Finseq-EQclass s ;
hence  not Finseq-EQclass s is empty ; ::_thesis: verum
end;
end;

theorem Th7: :: DIST_1:7
for S being finite set
for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff t in Finseq-EQclass s )
proof
let S be finite set ; ::_thesis: for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff t in Finseq-EQclass s )
let s, t be FinSequence of S; ::_thesis: ( s,t -are_prob_equivalent iff t in Finseq-EQclass s )
now__::_thesis:_(_t_in_Finseq-EQclass_s_implies_s,t_-are_prob_equivalent_)
assume  t in Finseq-EQclass s ; ::_thesis: s,t -are_prob_equivalent
then  ex t0 being FinSequence of S st
( t = t0 & s,t0 -are_prob_equivalent ) ;
hence  s,t -are_prob_equivalent ; ::_thesis: verum
end;
hence  ( s,t -are_prob_equivalent iff t in Finseq-EQclass s ) ; ::_thesis: verum
end;

theorem Th8: :: DIST_1:8
for S being finite set
for s being FinSequence of S holds s in Finseq-EQclass s ;

theorem Th9: :: DIST_1:9
for S being finite set
for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff Finseq-EQclass s = Finseq-EQclass t )
proof
let S be finite set ; ::_thesis: for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff Finseq-EQclass s = Finseq-EQclass t )
let t, s be FinSequence of S; ::_thesis: ( t,s -are_prob_equivalent iff Finseq-EQclass t = Finseq-EQclass s )
hereby  ::_thesis: ( Finseq-EQclass t = Finseq-EQclass s implies t,s -are_prob_equivalent )
assume A2: t,s -are_prob_equivalent ; ::_thesis: Finseq-EQclass t = Finseq-EQclass s
thus  Finseq-EQclass t = Finseq-EQclass s ::_thesis: verum
proof
thus  Finseq-EQclass t c= Finseq-EQclass s :: according to XBOOLE_0:def_10 ::_thesis: Finseq-EQclass s c= Finseq-EQclass t
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Finseq-EQclass t or x in Finseq-EQclass s )
assume  x in Finseq-EQclass t ; ::_thesis: x in Finseq-EQclass s
then consider u being FinSequence of S such that
A3: x = u and
A4: t,u -are_prob_equivalent ;
 s,u -are_prob_equivalent by A2, A4, Th6;
hence  x in Finseq-EQclass s by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Finseq-EQclass s or x in Finseq-EQclass t )
assume  x in Finseq-EQclass s ; ::_thesis: x in Finseq-EQclass t
then consider u being FinSequence of S such that
A6: x = u and
A7: s,u -are_prob_equivalent ;
 t,u -are_prob_equivalent by A2, A7, Th6;
hence  x in Finseq-EQclass t by A6; ::_thesis: verum
end;
end;
assume  Finseq-EQclass t = Finseq-EQclass s ; ::_thesis: t,s -are_prob_equivalent
then  t in Finseq-EQclass s ;
hence  t,s -are_prob_equivalent by Th7; ::_thesis: verum
end;

definition
let S be finite set ;
defpred S1[ set ] means  ex u being FinSequence of S st $1 = Finseq-EQclass u;
func distribution_family S ->  Subset-Family of (S *) means :Def6: :: DIST_1:def 6
 for A being Subset of (S *) holds
( A in it iff ex s being FinSequence of S st A = Finseq-EQclass s );
existence
 ex b1 being Subset-Family of (S *) st
for A being Subset of (S *) holds
( A in b1 iff ex s being FinSequence of S st A = Finseq-EQclass s )
proof
 ex T being Subset-Family of (S *) st
for A being Subset of (S *) holds
( A in T iff S1[A] ) from SUBSET_1:sch_3();
hence  ex b1 being Subset-Family of (S *) st
for A being Subset of (S *) holds
( A in b1 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of (S *) st ( for A being Subset of (S *) holds
( A in b1 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) & ( for A being Subset of (S *) holds
( A in b2 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) holds
b1 = b2
proof
let F1, F2 be Subset-Family of (S *); ::_thesis: ( ( for A being Subset of (S *) holds
( A in F1 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) & ( for A being Subset of (S *) holds
( A in F2 iff ex s being FinSequence of S st A = Finseq-EQclass s ) ) implies F1 = F2 )
assume that
A2: for A being Subset of (S *) holds
( A in F1 iff S1[A] ) and
A3: for A being Subset of (S *) holds
( A in F2 iff S1[A] ) ; ::_thesis: F1 = F2
thus  F1 = F2 from SUBSET_1:sch_4(A2, A3); ::_thesis: verum
end;
end;

:: deftheorem Def6 defines distribution_family DIST_1:def_6_:_
 for S being finite set
for b2 being Subset-Family of (S *) holds
( b2 = distribution_family S iff for A being Subset of (S *) holds
( A in b2 iff ex s being FinSequence of S st A = Finseq-EQclass s ) );

registration
let S be finite set ;
cluster distribution_family S ->  non empty ;
coherence
 not distribution_family S is empty
proof
 Finseq-EQclass the Element of S * in distribution_family S by Def6;
hence  not distribution_family S is empty ; ::_thesis: verum
end;
end;

theorem Th10: :: DIST_1:10
for S being finite set
for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )
proof
let S be finite set ; ::_thesis: for s, t being FinSequence of S holds
( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )
let s, t be FinSequence of S; ::_thesis: ( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t )
A1: now__::_thesis:_(_FDprobSEQ_s_=_FDprobSEQ_t_implies_s,t_-are_prob_equivalent_)
assume A2: FDprobSEQ s = FDprobSEQ t ; ::_thesis: s,t -are_prob_equivalent
 for x being set holds FDprobability (x,t) = FDprobability (x,s)
proof
let x be set ; ::_thesis: FDprobability (x,t) = FDprobability (x,s)
percases ( x in S or not x in S ) ;
suppose x in S ; ::_thesis: FDprobability (x,t) = FDprobability (x,s)
then  x in rng (canFS S) by FUNCT_2:def_3;
then consider n being set  such that
A3: n in dom (canFS S) and
A4: x = (canFS S) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A3;
 len (canFS S) = card S by UPROOTS:3;
then A5: n in Seg (card S) by A3, FINSEQ_1:def_3;
then A6: n in dom (FDprobSEQ t) by Def3;
 n in dom (FDprobSEQ s) by A5, Def3;
hence  FDprobability (x,s) = (FDprobSEQ s) . n by A4, Def3
.= FDprobability (x,t) by A2, A4, A6, Def3 ;
::_thesis: verum
end;
supposeA7: not x in S ; ::_thesis: FDprobability (x,t) = FDprobability (x,s)
 not x in rng t by A7;
then  rng t misses {x} by ZFMISC_1:50;
then A8: t " {x} = {} by RELAT_1:138;
 not x in rng s by A7;
then  rng s misses {x} by ZFMISC_1:50;
then  s " {x} = {} by RELAT_1:138;
hence  FDprobability (x,s) = 0
.= FDprobability (x,t) by A8 ;
::_thesis: verum
end;
end;
end;
hence  s,t -are_prob_equivalent by Def4; ::_thesis: verum
end;
now__::_thesis:_(_s,t_-are_prob_equivalent_implies_FDprobSEQ_s_=_FDprobSEQ_t_)
assume A13: s,t -are_prob_equivalent ; ::_thesis: FDprobSEQ s = FDprobSEQ t
A14: now__::_thesis:_for_n_being_Nat_st_n_in_dom_(FDprobSEQ_t)_holds_
(FDprobSEQ_t)_._n_=_FDprobability_(((canFS_S)_._n),s)
let n be Nat; ::_thesis: ( n in dom (FDprobSEQ t) implies (FDprobSEQ t) . n = FDprobability (((canFS S) . n),s) )
assume  n in dom (FDprobSEQ t) ; ::_thesis: (FDprobSEQ t) . n = FDprobability (((canFS S) . n),s)
hence (FDprobSEQ t) . n = FDprobability (((canFS S) . n),t) by Def3
.= FDprobability (((canFS S) . n),s) by A13, Def4 ;
::_thesis: verum
end;
 dom (FDprobSEQ t) = Seg (card S) by Def3;
hence  FDprobSEQ s = FDprobSEQ t by A14, Def3; ::_thesis: verum
end;
hence  ( s,t -are_prob_equivalent iff FDprobSEQ s = FDprobSEQ t ) by A1; ::_thesis: verum
end;

theorem :: DIST_1:11
for S being finite set
for s, t being FinSequence of S st t in Finseq-EQclass s holds
FDprobSEQ s = FDprobSEQ t
proof
let S be finite set ; ::_thesis: for s, t being FinSequence of S st t in Finseq-EQclass s holds
FDprobSEQ s = FDprobSEQ t
let s, t be FinSequence of S; ::_thesis: ( t in Finseq-EQclass s implies FDprobSEQ s = FDprobSEQ t )
assume  t in Finseq-EQclass s ; ::_thesis: FDprobSEQ s = FDprobSEQ t
then  ex w being FinSequence of S st
( t = w & s,w -are_prob_equivalent ) ;
hence  FDprobSEQ s = FDprobSEQ t by Th10; ::_thesis: verum
end;

definition
let S be finite set ;
func GenProbSEQ S ->  Function of (distribution_family S),(REAL *) means :Def7: :: DIST_1:def 7
 for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & it . x = FDprobSEQ s );
existence
 ex b1 being Function of (distribution_family S),(REAL *) st
for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & b1 . x = FDprobSEQ s )
proof
defpred S1[ set , set ] means  ex s being FinSequence of S st
( s in $1 & $2 = FDprobSEQ s );
A1: for x being Element of distribution_family S ex y being Element of REAL * st S1[x,y]
proof
let x be Element of distribution_family S; ::_thesis: ex y being Element of REAL * st S1[x,y]
consider s being FinSequence of S such that
A2: x = Finseq-EQclass s by Def6;
 FDprobSEQ s in REAL * by FINSEQ_1:def_11;
hence  ex y being Element of REAL * st S1[x,y] by A2, Th8; ::_thesis: verum
end;
consider g being Function of (distribution_family S),(REAL *) such that
A3: for x being Element of distribution_family S holds S1[x,g . x] from FUNCT_2:sch_3(A1);
take  g ; ::_thesis: for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s )
thus  for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s ) by A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (distribution_family S),(REAL *) st ( for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & b1 . x = FDprobSEQ s ) ) & ( for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & b2 . x = FDprobSEQ s ) ) holds
b1 = b2
proof
let g, h be Function of (distribution_family S),(REAL *); ::_thesis: ( ( for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s ) ) & ( for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & h . x = FDprobSEQ s ) ) implies g = h )
assume A4: for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s ) ; ::_thesis: ( ex x being Element of distribution_family S st
for s being FinSequence of S holds
( not s in x or not h . x = FDprobSEQ s ) or g = h )
assume A5: for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & h . x = FDprobSEQ s ) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_distribution_family_S_holds_g_._x_=_h_._x
let x be Element of distribution_family S; ::_thesis: g . x = h . x
consider u being FinSequence of S such that
A6: x = Finseq-EQclass u by Def6;
consider t being FinSequence of S such that
A7: t in x and
A8: h . x = FDprobSEQ t by A5;
A9: t,u -are_prob_equivalent by A6, A7, Th7;
consider s being FinSequence of S such that
A10: s in x and
A11: g . x = FDprobSEQ s by A4;
 u,s -are_prob_equivalent by A6, A10, Th7;
then  t,s -are_prob_equivalent by A9, Th6;
hence  g . x = h . x by A11, A8, Th10; ::_thesis: verum
end;
hence  g = h by FUNCT_2:def_8; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines GenProbSEQ DIST_1:def_7_:_
 for S being finite set
for b2 being Function of (distribution_family S),(REAL *) holds
( b2 = GenProbSEQ S iff for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & b2 . x = FDprobSEQ s ) );

theorem Th12: :: DIST_1:12
for S being finite set
for s being FinSequence of S holds (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s
proof
let S be finite set ; ::_thesis: for s being FinSequence of S holds (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s
let s be FinSequence of S; ::_thesis: (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s
 Finseq-EQclass s is Element of distribution_family S by Def6;
then consider u being FinSequence of S such that
A1: u in Finseq-EQclass s and
A2: (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ u by Def7;
 s,u -are_prob_equivalent by A1, Th7;
hence  (GenProbSEQ S) . (Finseq-EQclass s) = FDprobSEQ s by A2, Th10; ::_thesis: verum
end;

registration
let S be finite set ;
cluster GenProbSEQ S ->  one-to-one ;
coherence
 GenProbSEQ S is one-to-one
proof
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_distribution_family_S_&_x2_in_distribution_family_S_&_(GenProbSEQ_S)_._x1_=_(GenProbSEQ_S)_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in distribution_family S & x2 in distribution_family S & (GenProbSEQ S) . x1 = (GenProbSEQ S) . x2 implies x1 = x2 )
assume that
A1: x1 in distribution_family S and
A2: x2 in distribution_family S and
A3: (GenProbSEQ S) . x1 = (GenProbSEQ S) . x2 ; ::_thesis: x1 = x2
consider u1 being FinSequence of S such that
A4: x1 = Finseq-EQclass u1 by A1, Def6;
consider u2 being FinSequence of S such that
A5: x2 = Finseq-EQclass u2 by A2, Def6;
consider v being FinSequence of S such that
A6: v in x2 and
A7: (GenProbSEQ S) . x2 = FDprobSEQ v by A2, Def7;
consider u being FinSequence of S such that
A8: u in x1 and
A9: (GenProbSEQ S) . x1 = FDprobSEQ u by A1, Def7;
A10: u,v -are_prob_equivalent by A3, A9, A7, Th10;
 u1,u -are_prob_equivalent by A8, A4, Th7;
then A11: u1,v -are_prob_equivalent by A10, Th6;
 v,u2 -are_prob_equivalent by A6, A5, Th7;
then  u1,u2 -are_prob_equivalent by A11, Th6;
hence  x1 = x2 by A4, A5, Th9; ::_thesis: verum
end;
hence  GenProbSEQ S is one-to-one by FUNCT_2:19; ::_thesis: verum
end;
end;

definition
let S be finite set ;
let p be ProbFinS FinSequence of REAL ;
assume A1: ex s being FinSequence of S st FDprobSEQ s = p ;
func distribution (p,S) ->  Element of distribution_family S means :Def8: :: DIST_1:def 8
(GenProbSEQ S) . it = p;
existence
 ex b1 being Element of distribution_family S st (GenProbSEQ S) . b1 = p
proof
consider s being FinSequence of S such that
A2: FDprobSEQ s = p by A1;
reconsider CS = Finseq-EQclass s as Element of distribution_family S by Def6;
take  CS ; ::_thesis: (GenProbSEQ S) . CS = p
thus  (GenProbSEQ S) . CS = p by A2, Th12; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of distribution_family S st (GenProbSEQ S) . b1 = p & (GenProbSEQ S) . b2 = p holds
b1 = b2
proof
let CS1, CS2 be Element of distribution_family S; ::_thesis: ( (GenProbSEQ S) . CS1 = p & (GenProbSEQ S) . CS2 = p implies CS1 = CS2 )
assume A4: (GenProbSEQ S) . CS1 = p ; ::_thesis: ( not (GenProbSEQ S) . CS2 = p or CS1 = CS2 )
then A5: CS1 in dom (GenProbSEQ S) by FUNCT_1:def_2;
assume A6: (GenProbSEQ S) . CS2 = p ; ::_thesis: CS1 = CS2
then  CS2 in dom (GenProbSEQ S) by FUNCT_1:def_2;
hence  CS1 = CS2 by A4, A6, A5, FUNCT_1:def_4; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines distribution DIST_1:def_8_:_
 for S being finite set
for p being ProbFinS FinSequence of REAL st ex s being FinSequence of S st FDprobSEQ s = p holds
for b3 being Element of distribution_family S holds
( b3 = distribution (p,S) iff (GenProbSEQ S) . b3 = p );

definition
let S be finite set ;
let s be FinSequence of S;
func freqSEQ s ->  FinSequence of NAT  means :Def9: :: DIST_1:def 9
( dom it = Seg (card S) & ( for n being Nat st n in dom it holds
it . n = (len s) * ((FDprobSEQ s) . n) ) );
existence
 ex b1 being FinSequence of NAT st
( dom b1 = Seg (card S) & ( for n being Nat st n in dom b1 holds
b1 . n = (len s) * ((FDprobSEQ s) . n) ) )
proof
defpred S1[ Nat, set ] means $2 = (len s) * ((FDprobSEQ s) . $1);
A1: for k being Nat st k in Seg (card S) holds
ex x being Element of NAT st S1[k,x]
proof
A2: rng (canFS S) = S by FUNCT_2:def_3;
let k be Nat; ::_thesis: ( k in Seg (card S) implies ex x being Element of NAT st S1[k,x] )
assume A3: k in Seg (card S) ; ::_thesis: ex x being Element of NAT st S1[k,x]
 Seg (len (canFS S)) = Seg (card S) by UPROOTS:3;
then  k in dom (canFS S) by A3, FINSEQ_1:def_3;
then  (canFS S) . k is Element of S by A2, FUNCT_1:3;
then consider a being Element of S such that
A4: a = (canFS S) . k ;
set y = (len s) * ((FDprobSEQ s) . k);
take  (len s) * ((FDprobSEQ s) . k) ; ::_thesis: ( (len s) * ((FDprobSEQ s) . k) is Element of NAT & S1[k,(len s) * ((FDprobSEQ s) . k)] )
 k in dom (FDprobSEQ s) by A3, Def3;
then A6: (len s) * ((FDprobSEQ s) . k) = (len s) * (FDprobability (a,s)) by A4, Def3;
 (len s) * ((FDprobSEQ s) . k) is Element of NAT
proof
percases ( s = {} or s <> {} ) ;
suppose s = {} ; ::_thesis: (len s) * ((FDprobSEQ s) . k) is Element of NAT
hence  (len s) * ((FDprobSEQ s) . k) is Element of NAT by A6; ::_thesis: verum
end;
suppose s <> {} ; ::_thesis: (len s) * ((FDprobSEQ s) . k) is Element of NAT
hence  (len s) * ((FDprobSEQ s) . k) is Element of NAT by A6, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence  ( (len s) * ((FDprobSEQ s) . k) is Element of NAT & S1[k,(len s) * ((FDprobSEQ s) . k)] ) ; ::_thesis: verum
end;
consider g being FinSequence of NAT  such that
A7: ( dom g = Seg (card S) & ( for n being Nat st n in Seg (card S) holds
S1[n,g . n] ) ) from FINSEQ_1:sch_5(A1);
take  g ; ::_thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ) )
thus  ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ) ) by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of NAT st dom b1 = Seg (card S) & ( for n being Nat st n in dom b1 holds
b1 . n = (len s) * ((FDprobSEQ s) . n) ) & dom b2 = Seg (card S) & ( for n being Nat st n in dom b2 holds
b2 . n = (len s) * ((FDprobSEQ s) . n) ) holds
b1 = b2
proof
let g, h be FinSequence of NAT ; ::_thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ) & dom h = Seg (card S) & ( for n being Nat st n in dom h holds
h . n = (len s) * ((FDprobSEQ s) . n) ) implies g = h )
assume that
A8: dom g = Seg (card S) and
A9: for n being Nat st n in dom g holds
g . n = (len s) * ((FDprobSEQ s) . n) ; ::_thesis: ( not dom h = Seg (card S) or ex n being Nat st
( n in dom h & not h . n = (len s) * ((FDprobSEQ s) . n) ) or g = h )
assume that
A10: dom h = Seg (card S) and
A11: for n being Nat st n in dom h holds
h . n = (len s) * ((FDprobSEQ s) . n) ; ::_thesis: g = h
A12: now__::_thesis:_for_n_being_Nat_st_n_in_dom_g_holds_
g_._n_=_h_._n
let n be Nat; ::_thesis: ( n in dom g implies g . n = h . n )
assume A13: n in dom g ; ::_thesis: g . n = h . n
hence g . n = (len s) * ((FDprobSEQ s) . n) by A9
.= h . n by A8, A10, A11, A13 ;
::_thesis: verum
end;
len g = card S by A8, FINSEQ_1:def_3
.= len h by A10, FINSEQ_1:def_3 ;
hence  g = h by A12, FINSEQ_2:9; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines freqSEQ DIST_1:def_9_:_
 for S being finite set
for s being FinSequence of S
for b3 being FinSequence of NAT holds
( b3 = freqSEQ s iff ( dom b3 = Seg (card S) & ( for n being Nat st n in dom b3 holds
b3 . n = (len s) * ((FDprobSEQ s) . n) ) ) );

theorem Th13: :: DIST_1:13
for S being non empty finite set
for s being non empty FinSequence of S
for n being Nat st n in Seg (card S) holds
ex x being Element of S st
( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n )
proof
let S be non empty finite set ; ::_thesis: for s being non empty FinSequence of S
for n being Nat st n in Seg (card S) holds
ex x being Element of S st
( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n )
let s be non empty FinSequence of S; ::_thesis: for n being Nat st n in Seg (card S) holds
ex x being Element of S st
( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n )
let n be Nat; ::_thesis: ( n in Seg (card S) implies ex x being Element of S st
( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n ) )
set y = (len s) * ((FDprobSEQ s) . n);
A2: rng (canFS S) = S by FUNCT_2:def_3;
assume A3: n in Seg (card S) ; ::_thesis: ex x being Element of S st
( (freqSEQ s) . n = frequency (x,s) & x = (canFS S) . n )
then A4: n in dom (freqSEQ s) by Def9;
 Seg (len (canFS S)) = Seg (card S) by UPROOTS:3;
then  n in dom (canFS S) by A3, FINSEQ_1:def_3;
then  (canFS S) . n is Element of S by A2, FUNCT_1:3;
then consider a being Element of S such that
A5: a = (canFS S) . n ;
take  a ; ::_thesis: ( (freqSEQ s) . n = frequency (a,s) & a = (canFS S) . n )
 n in dom (FDprobSEQ s) by A3, Def3;
then  (len s) * ((FDprobSEQ s) . n) = (len s) * (FDprobability (a,s)) by A5, Def3;
then  (len s) * ((FDprobSEQ s) . n) = frequency (a,s) by XCMPLX_1:87;
hence  ( (freqSEQ s) . n = frequency (a,s) & a = (canFS S) . n ) by A4, A5, Def9; ::_thesis: verum
end;

theorem Th14: :: DIST_1:14
for S being finite set
for s being FinSequence of S holds freqSEQ s = (len s) * (FDprobSEQ s)
proof
let S be finite set ; ::_thesis: for s being FinSequence of S holds freqSEQ s = (len s) * (FDprobSEQ s)
let s be FinSequence of S; ::_thesis: freqSEQ s = (len s) * (FDprobSEQ s)
A1: dom ((len s) (#) (FDprobSEQ s)) = dom (FDprobSEQ s) by VALUED_1:def_5
.= Seg (card S) by Def3
.= dom (freqSEQ s) by Def9 ;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_((len_s)_(#)_(FDprobSEQ_s))_holds_
((len_s)_(#)_(FDprobSEQ_s))_._m_=_(freqSEQ_s)_._m
let m be Nat; ::_thesis: ( m in dom ((len s) (#) (FDprobSEQ s)) implies ((len s) (#) (FDprobSEQ s)) . m = (freqSEQ s) . m )
assume A2: m in dom ((len s) (#) (FDprobSEQ s)) ; ::_thesis: ((len s) (#) (FDprobSEQ s)) . m = (freqSEQ s) . m
hence ((len s) (#) (FDprobSEQ s)) . m = (len s) * ((FDprobSEQ s) . m) by VALUED_1:def_5
.= (freqSEQ s) . m by A1, A2, Def9 ;
::_thesis: verum
end;
hence  freqSEQ s = (len s) (#) (FDprobSEQ s) by A1, FINSEQ_1:13; ::_thesis: verum
end;

theorem Th15: :: DIST_1:15
for S being finite set
for s being FinSequence of S holds Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))
proof
let S be finite set ; ::_thesis: for s being FinSequence of S holds Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))
let s be FinSequence of S; ::_thesis: Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s))
 freqSEQ s = (len s) * (FDprobSEQ s) by Th14;
hence  Sum (freqSEQ s) = (len s) * (Sum (FDprobSEQ s)) by RVSUM_1:87; ::_thesis: verum
end;

theorem :: DIST_1:16
for S being non empty finite set
for s being non empty FinSequence of S
for n being Nat st n in dom s holds
ex m being Nat st
( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
proof
let S be non empty finite set ; ::_thesis: for s being non empty FinSequence of S
for n being Nat st n in dom s holds
ex m being Nat st
( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
let s be non empty FinSequence of S; ::_thesis: for n being Nat st n in dom s holds
ex m being Nat st
( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
let n be Nat; ::_thesis: ( n in dom s implies ex m being Nat st
( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m ) )
set x = s . n;
assume  n in dom s ; ::_thesis: ex m being Nat st
( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
then  s . n in rng s by FUNCT_1:3;
then  s . n in S ;
then  s . n in rng (canFS S) by FUNCT_2:def_3;
then consider m being set  such that
A1: m in dom (canFS S) and
A2: s . n = (canFS S) . m by FUNCT_1:def_3;
reconsider m = m as Nat by A1;
take  m ; ::_thesis: ( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m )
 Seg (len (canFS S)) = Seg (card S) by UPROOTS:3;
then  dom (canFS S) = Seg (card S) by FINSEQ_1:def_3;
then  ex xx being Element of S st
( (freqSEQ s) . m = frequency (xx,s) & xx = (canFS S) . m ) by A1, Th13;
hence  ( (freqSEQ s) . m = frequency ((s . n),s) & s . n = (canFS S) . m ) by A2; ::_thesis: verum
end;

Lem1:  for S being Function
for X being set st S is disjoint_valued holds
S | X is disjoint_valued
proof
let S be Function; ::_thesis: for X being set st S is disjoint_valued holds
S | X is disjoint_valued
let X be set ; ::_thesis: ( S is disjoint_valued implies S | X is disjoint_valued )
assume A3: S is disjoint_valued ; ::_thesis: S | X is disjoint_valued
set SN = S | X;
now__::_thesis:_for_x,_y_being_set_st_x_<>_y_holds_
(S_|_X)_._x_misses_(S_|_X)_._y
let x, y be set ; ::_thesis: ( x <> y implies (S | X) . b1 misses (S | X) . b2 )
assume A30: x <> y ; ::_thesis: (S | X) . b1 misses (S | X) . b2
percases ( ( x in dom (S | X) & y in dom (S | X) ) or not x in dom (S | X) or not y in dom (S | X) ) ;
suppose ( x in dom (S | X) & y in dom (S | X) ) ; ::_thesis: (S | X) . b1 misses (S | X) . b2
then  ( (S | X) . x = S . x & (S | X) . y = S . y ) by FUNCT_1:47;
hence  (S | X) . x misses (S | X) . y by A3, A30, PROB_2:def_2; ::_thesis: verum
end;
supposeA31: ( not x in dom (S | X) or not y in dom (S | X) ) ; ::_thesis: (S | X) . b1 misses (S | X) . b2
now__::_thesis:_(S_|_X)_._x_misses_(S_|_X)_._y
percases ( not x in dom (S | X) or not y in dom (S | X) ) by A31;
suppose not x in dom (S | X) ; ::_thesis: (S | X) . x misses (S | X) . y
then  (S | X) . x = {} by FUNCT_1:def_2;
then  ((S | X) . x) /\ ((S | X) . y) = {} ;
hence  (S | X) . x misses (S | X) . y by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose not y in dom (S | X) ; ::_thesis: (S | X) . x misses (S | X) . y
then  (S | X) . y = {} by FUNCT_1:def_2;
then  ((S | X) . x) /\ ((S | X) . y) = {} ;
hence  (S | X) . x misses (S | X) . y by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence  (S | X) . x misses (S | X) . y ; ::_thesis: verum
end;
end;
end;
hence  S | X is disjoint_valued by PROB_2:def_2; ::_thesis: verum
end;

Th17:  for n being Nat
for S being Function
for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & n = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
proof
defpred S1[ Nat] means  for S being Function
for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & $1 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L );
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_S_being_Function
for_L_being_FinSequence_of_NAT_st_S_is_disjoint_valued_&_dom_S_=_dom_L_&_n_+_1_=_len_L_&_(_for_i_being_Nat_st_i_in_dom_S_holds_
(_S_._i_is_finite_&_L_._i_=_card_(S_._i)_)_)_holds_
(_Union_S_is_finite_&_card_(Union_S)_=_Sum_L_)
let S be Function; ::_thesis: for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & n + 1 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
let L be FinSequence of NAT ; ::_thesis: ( S is disjoint_valued & dom S = dom L & n + 1 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) implies ( Union S is finite & card (Union S) = Sum L ) )
assume that
A3: S is disjoint_valued and
A4: dom S = dom L and
A5: n + 1 = len L and
A6: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ; ::_thesis: ( Union S is finite & card (Union S) = Sum L )
set SN = S | (Seg n);
reconsider LN = L | n as FinSequence of NAT ;
A7: n = len LN by A5, FINSEQ_1:59, NAT_1:12;
now__::_thesis:_for_x_being_set_st_x_in_Union_S_holds_
x_in_(Union_(S_|_(Seg_n)))_\/_(S_._(n_+_1))
let x be set ; ::_thesis: ( x in Union S implies x in (Union (S | (Seg n))) \/ (S . (n + 1)) )
assume  x in Union S ; ::_thesis: x in (Union (S | (Seg n))) \/ (S . (n + 1))
then consider y being set  such that
A8: x in y and
A9: y in rng S by TARSKI:def_4;
consider i being set  such that
A10: i in dom S and
A11: y = S . i by A9, FUNCT_1:def_3;
A12: i in Seg (n + 1) by A4, A5, A10, FINSEQ_1:def_3;
reconsider i = i as Element of NAT by A4, A10;
A13: i <= n + 1 by A12, FINSEQ_1:1;
A14: 1 <= i by A12, FINSEQ_1:1;
now__::_thesis:_x_in_(Union_(S_|_(Seg_n)))_\/_(S_._(n_+_1))
percases ( i = n + 1 or i <> n + 1 ) ;
suppose i = n + 1 ; ::_thesis: x in (Union (S | (Seg n))) \/ (S . (n + 1))
hence  x in (Union (S | (Seg n))) \/ (S . (n + 1)) by A8, A11, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose i <> n + 1 ; ::_thesis: x in (Union (S | (Seg n))) \/ (S . (n + 1))
then  i < n + 1 by A13, XXREAL_0:1;
then  i <= n by NAT_1:13;
then  i in Seg n by A14;
then  i in (dom S) /\ (Seg n) by A10, XBOOLE_0:def_4;
then A15: i in dom (S | (Seg n)) by RELAT_1:61;
then  S . i = (S | (Seg n)) . i by FUNCT_1:47;
then  y in rng (S | (Seg n)) by A11, A15, FUNCT_1:def_3;
then  x in Union (S | (Seg n)) by A8, TARSKI:def_4;
hence  x in (Union (S | (Seg n))) \/ (S . (n + 1)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  x in (Union (S | (Seg n))) \/ (S . (n + 1)) ; ::_thesis: verum
end;
then A16: Union S c= (Union (S | (Seg n))) \/ (S . (n + 1)) by TARSKI:def_3;
A17: (Union (S | (Seg n))) \/ (S . (n + 1)) c= Union S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union (S | (Seg n))) \/ (S . (n + 1)) or x in Union S )
assume A18: x in (Union (S | (Seg n))) \/ (S . (n + 1)) ; ::_thesis: x in Union S
now__::_thesis:_x_in_Union_S
percases ( x in S . (n + 1) or x in Union (S | (Seg n)) ) by A18, XBOOLE_0:def_3;
supposeA19: x in S . (n + 1) ; ::_thesis: x in Union S
 n + 1 in Seg (n + 1) by FINSEQ_1:4;
then  n + 1 in dom S by A4, A5, FINSEQ_1:def_3;
then  S . (n + 1) in rng S by FUNCT_1:def_3;
hence  x in Union S by A19, TARSKI:def_4; ::_thesis: verum
end;
suppose x in Union (S | (Seg n)) ; ::_thesis: x in Union S
then consider y being set  such that
A20: x in y and
A21: y in rng (S | (Seg n)) by TARSKI:def_4;
consider i being set  such that
A22: i in dom (S | (Seg n)) and
A23: y = (S | (Seg n)) . i by A21, FUNCT_1:def_3;
 i in (dom S) /\ (Seg n) by A22, RELAT_1:61;
then A24: i in dom S by XBOOLE_0:def_4;
 (S | (Seg n)) . i = S . i by A22, FUNCT_1:47;
then  y in rng S by A23, A24, FUNCT_1:def_3;
hence  x in Union S by A20, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence  x in Union S ; ::_thesis: verum
end;
then A25: (Union (S | (Seg n))) \/ (S . (n + 1)) = Union S by A16, XBOOLE_0:def_10;
A26: for i being Nat st i in dom (S | (Seg n)) holds
( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) )
proof
let i be Nat; ::_thesis: ( i in dom (S | (Seg n)) implies ( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) ) )
assume A27: i in dom (S | (Seg n)) ; ::_thesis: ( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) )
then A28: i in (dom S) /\ (Seg n) by RELAT_1:61;
then A29: i in dom S by XBOOLE_0:def_4;
LN . i = L . i by A4, A28, FUNCT_1:48
.= card (S . i) by A6, A29
.= card ((S | (Seg n)) . i) by A27, FUNCT_1:47 ;
hence  ( (S | (Seg n)) . i is finite & LN . i = card ((S | (Seg n)) . i) ) ; ::_thesis: verum
end;
A32: S | (Seg n) is disjoint_valued by Lem1, A3;
A33: dom (S | (Seg n)) = (dom S) /\ (Seg n) by RELAT_1:61
.= dom LN by A4, RELAT_1:61 ;
then A34: card (Union (S | (Seg n))) = Sum LN by A2, A32, A7, A26;
reconsider USN = Union (S | (Seg n)) as finite set by A2, A32, A33, A7, A26;
A35: 1 <= n + 1 by NAT_1:11;
A36: L = (L | n) ^ <*(L /. (len L))*> by A5, FINSEQ_5:21
.= LN ^ <*(L . (n + 1))*> by A5, A35, FINSEQ_4:15 ;
 n + 1 in Seg (len L) by A5, FINSEQ_1:4;
then A37: n + 1 in dom S by A4, FINSEQ_1:def_3;
then reconsider S1 = S . (n + 1) as finite set by A6;
 Union S = USN \/ S1 by A16, A17, XBOOLE_0:def_10;
hence  Union S is finite ; ::_thesis: card (Union S) = Sum L
 for z being set st z in rng (S | (Seg n)) holds
z misses S . (n + 1)
proof
let y be set ; ::_thesis: ( y in rng (S | (Seg n)) implies y misses S . (n + 1) )
assume  y in rng (S | (Seg n)) ; ::_thesis: y misses S . (n + 1)
then consider i being set  such that
A38: i in dom (S | (Seg n)) and
A39: y = (S | (Seg n)) . i by FUNCT_1:def_3;
A40: i in (dom S) /\ (Seg n) by A38, RELAT_1:61;
then A41: i in Seg n by XBOOLE_0:def_4;
reconsider i = i as Element of NAT by A40;
 i <= n by A41, FINSEQ_1:1;
then A42: i <> n + 1 by NAT_1:13;
 y = S . i by A38, A39, FUNCT_1:47;
hence  y misses S . (n + 1) by A3, A42, PROB_2:def_2; ::_thesis: verum
end;
then  Union (S | (Seg n)) misses S . (n + 1) by ZFMISC_1:80;
then  card ((Union (S | (Seg n))) \/ (S . (n + 1))) = (card USN) + (card S1) by CARD_2:40;
hence  card (Union S) = (Sum LN) + (L . (n + 1)) by A6, A37, A34, A25
.= Sum L by A36, RVSUM_1:74 ;
::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A43: S1[ 0 ]
proof
let S be Function; ::_thesis: for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & 0 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
let L be FinSequence of NAT ; ::_thesis: ( S is disjoint_valued & dom S = dom L & 0 = len L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) implies ( Union S is finite & card (Union S) = Sum L ) )
assume that
 S is disjoint_valued and
A44: dom S = dom L and
A45: 0 = len L and
 for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ; ::_thesis: ( Union S is finite & card (Union S) = Sum L )
A46: L = {} by A45;
then  S = {} by A44;
then  for X being set st X in rng S holds
X c= {} ;
then  Union S c= {} by ZFMISC_1:76;
hence  ( Union S is finite & card (Union S) = Sum L ) by A46, RVSUM_1:72; ::_thesis: verum
end;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A43, A1); ::_thesis: verum
end;

theorem Th18: :: DIST_1:17
for S being Function
for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
proof
let S be Function; ::_thesis: for L being FinSequence of NAT st S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) holds
( Union S is finite & card (Union S) = Sum L )
let L be FinSequence of NAT ; ::_thesis: ( S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) implies ( Union S is finite & card (Union S) = Sum L ) )
A1: len L is Element of NAT ;
assume  ( S is disjoint_valued & dom S = dom L & ( for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) ) ) ; ::_thesis: ( Union S is finite & card (Union S) = Sum L )
hence  ( Union S is finite & card (Union S) = Sum L ) by A1, Th17; ::_thesis: verum
end;

theorem Th19: :: DIST_1:18
for S being non empty finite set
for s being non empty FinSequence of S holds Sum (freqSEQ s) = len s
proof
let S be non empty finite set ; ::_thesis: for s being non empty FinSequence of S holds Sum (freqSEQ s) = len s
let s be non empty FinSequence of S; ::_thesis: Sum (freqSEQ s) = len s
set L = freqSEQ s;
defpred S1[ set , set ] means  ex z being Element of S st
( z = (canFS S) . $1 & $2 = event_pick (z,s) );
 len (canFS S) = card S by UPROOTS:3;
then A1: dom (canFS S) = Seg (card S) by FINSEQ_1:def_3;
A2: for x being set st x in dom (freqSEQ s) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom (freqSEQ s) implies ex y being set st S1[x,y] )
set z = (canFS S) . x;
assume  x in dom (freqSEQ s) ; ::_thesis: ex y being set st S1[x,y]
then A3: x in Seg (card S) by Def9;
 rng (canFS S) = S by FUNCT_2:def_3;
then reconsider z = (canFS S) . x as Element of S by A1, A3, FUNCT_1:3;
set y = s " {z};
take  s " {z} ; ::_thesis: S1[x,s " {z}]
 s " {z} = event_pick (z,s) ;
hence  S1[x,s " {z}] ; ::_thesis: verum
end;
consider T being Function such that
A5: ( dom T = dom (freqSEQ s) & ( for x being set st x in dom (freqSEQ s) holds
S1[x,T . x] ) ) from CLASSES1:sch_1(A2);
A6: for a, b being set st a in dom T & b in dom T & a <> b holds
T . a misses T . b
proof
let a, b be set ; ::_thesis: ( a in dom T & b in dom T & a <> b implies T . a misses T . b )
assume that
A7: ( a in dom T & b in dom T ) and
A8: a <> b ; ::_thesis: T . a misses T . b
 ( a in dom (canFS S) & b in dom (canFS S) ) by A1, A5, A7, Def9;
then A9: (canFS S) . a <> (canFS S) . b by A8, FUNCT_1:def_4;
 ( ex za being Element of S st
( za = (canFS S) . a & T . a = event_pick (za,s) ) & ex zb being Element of S st
( zb = (canFS S) . b & T . b = event_pick (zb,s) ) ) by A5, A7;
hence  T . a misses T . b by A9, FUNCT_1:71, ZFMISC_1:11; ::_thesis: verum
end;
 for a, b being set st a <> b holds
T . a misses T . b
proof
let a, b be set ; ::_thesis: ( a <> b implies T . a misses T . b )
assume A10: a <> b ; ::_thesis: T . a misses T . b
percases ( ( a in dom T & b in dom T ) or not a in dom T or ( a in dom T & not b in dom T ) ) ;
suppose ( a in dom T & b in dom T ) ; ::_thesis: T . a misses T . b
hence  T . a misses T . b by A6, A10; ::_thesis: verum
end;
suppose not a in dom T ; ::_thesis: T . a misses T . b
then  T . a = {} by FUNCT_1:def_2;
hence  T . a misses T . b by XBOOLE_1:65; ::_thesis: verum
end;
suppose ( a in dom T & not b in dom T ) ; ::_thesis: T . a misses T . b
then  T . b = {} by FUNCT_1:def_2;
hence  T . a misses T . b by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
then A11: T is disjoint_valued by PROB_2:def_2;
A12: Seg (len s) c= Union T
proof
assume  not Seg (len s) c= Union T ; ::_thesis: contradiction
then consider ne being set  such that
A13: ne in Seg (len s) and
A14: not ne in Union T by TARSKI:def_3;
set yne = s . ne;
A15: ne in dom s by A13, FINSEQ_1:def_3;
then  s . ne in rng s by FUNCT_1:def_3;
then reconsider yne = s . ne as Element of S ;
 rng (canFS S) = S by FUNCT_2:def_3;
then consider nne being set  such that
A16: nne in dom (canFS S) and
A17: yne = (canFS S) . nne by FUNCT_1:def_3;
A18: nne in dom (freqSEQ s) by A1, A16, Def9;
then A19: T . nne in rng T by A5, FUNCT_1:3;
A20: s . ne in {(s . ne)} by TARSKI:def_1;
 ex zne being Element of S st
( zne = (canFS S) . nne & T . nne = event_pick (zne,s) ) by A5, A18;
then  ne in T . nne by A15, A17, A20, FUNCT_1:def_7;
hence  contradiction by A14, A19, TARSKI:def_4; ::_thesis: verum
end;
A21: for i being Nat st i in dom T holds
( T . i is finite & (freqSEQ s) . i = card (T . i) )
proof
let i be Nat; ::_thesis: ( i in dom T implies ( T . i is finite & (freqSEQ s) . i = card (T . i) ) )
assume A22: i in dom T ; ::_thesis: ( T . i is finite & (freqSEQ s) . i = card (T . i) )
then A23: ex zi being Element of S st
( zi = (canFS S) . i & T . i = event_pick (zi,s) ) by A5;
 dom (freqSEQ s) = Seg (card S) by Def9;
then A24: i in dom (FDprobSEQ s) by A5, A22, Def3;
(freqSEQ s) . i = (len s) * ((FDprobSEQ s) . i) by A5, A22, Def9
.= (len s) * (FDprobability (((canFS S) . i),s)) by A24, Def3
.= card (T . i) by A23, XCMPLX_1:87 ;
hence  ( T . i is finite & (freqSEQ s) . i = card (T . i) ) ; ::_thesis: verum
end;
then reconsider T1 = Union T as finite set by A5, A11, Th18;
 for X being set st X in rng T holds
X c= Seg (len s)
proof
let X be set ; ::_thesis: ( X in rng T implies X c= Seg (len s) )
assume  X in rng T ; ::_thesis: X c= Seg (len s)
then consider j being set  such that
A25: j in dom T and
A26: X = T . j by FUNCT_1:def_3;
 ex zj being Element of S st
( zj = (canFS S) . j & T . j = event_pick (zj,s) ) by A5, A25;
then  X c= whole_event by A26;
hence  X c= Seg (len s) by FINSEQ_1:def_3; ::_thesis: verum
end;
then  Union T c= Seg (len s) by ZFMISC_1:76;
then A27: T1 = Seg (len s) by A12, XBOOLE_0:def_10;
thus  Sum (freqSEQ s) = card T1 by A5, A11, A21, Th18
.= len s by A27, FINSEQ_1:57 ; ::_thesis: verum
end;

theorem Th20: :: DIST_1:19
for S being non empty finite set
for s being non empty FinSequence of S holds Sum (FDprobSEQ s) = 1
proof
let S be non empty finite set ; ::_thesis: for s being non empty FinSequence of S holds Sum (FDprobSEQ s) = 1
let s be non empty FinSequence of S; ::_thesis: Sum (FDprobSEQ s) = 1
 Sum (freqSEQ s) = len s by Th19;
then  (len s) * (Sum (FDprobSEQ s)) = (len s) * 1 by Th15;
hence  Sum (FDprobSEQ s) = 1 by XCMPLX_1:5; ::_thesis: verum
end;

registration
let S be non empty finite set ;
let s be non empty FinSequence of S;
cluster FDprobSEQ s ->  ProbFinS ;
coherence
 FDprobSEQ s is ProbFinS
proof
A1: for i being Element of NAT st i in dom (FDprobSEQ s) holds
(FDprobSEQ s) . i >= 0
proof
let i be Element of NAT ; ::_thesis: ( i in dom (FDprobSEQ s) implies (FDprobSEQ s) . i >= 0 )
assume  i in dom (FDprobSEQ s) ; ::_thesis: (FDprobSEQ s) . i >= 0
then  (FDprobSEQ s) . i = FDprobability (((canFS S) . i),s) by Def3;
hence  (FDprobSEQ s) . i >= 0 ; ::_thesis: verum
end;
 Sum (FDprobSEQ s) = 1 by Th20;
hence  FDprobSEQ s is ProbFinS by A1, MATRPROB:def_5; ::_thesis: verum
end;
end;

definition
let S be non empty finite set ;
mode distProbFinS of S ->  ProbFinS FinSequence of REAL  means :Def10: :: DIST_1:def 10
( len it = card S & ex s being FinSequence of S st FDprobSEQ s = it );
existence
 ex b1 being ProbFinS FinSequence of REAL st
( len b1 = card S & ex s being FinSequence of S st FDprobSEQ s = b1 )
proof
set a = the Element of S;
set s = <* the Element of S*>;
set p = FDprobSEQ <* the Element of S*>;
 dom (FDprobSEQ <* the Element of S*>) = Seg (card S) by Def3;
then  len (FDprobSEQ <* the Element of S*>) = card S by FINSEQ_1:def_3;
hence  ex b1 being ProbFinS FinSequence of REAL st
( len b1 = card S & ex s being FinSequence of S st FDprobSEQ s = b1 ) ; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines distProbFinS DIST_1:def_10_:_
 for S being non empty finite set
for b2 being ProbFinS FinSequence of REAL holds
( b2 is distProbFinS of S iff ( len b2 = card S & ex s being FinSequence of S st FDprobSEQ s = b2 ) );

theorem Th22: :: DIST_1:20
for S being non empty finite set
for p being distProbFinS of S holds
( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
proof
let S be non empty finite set ; ::_thesis: for p being distProbFinS of S holds
( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
let p be distProbFinS of S; ::_thesis: ( distribution (p,S) is Element of distribution_family S & (GenProbSEQ S) . (distribution (p,S)) = p )
thus  distribution (p,S) is Element of distribution_family S ; ::_thesis: (GenProbSEQ S) . (distribution (p,S)) = p
 ex s being FinSequence of S st FDprobSEQ s = p by Def10;
hence  (GenProbSEQ S) . (distribution (p,S)) = p by Def8; ::_thesis: verum
end;

begin

definition
let S be finite set ;
let s be FinSequence of S;
attrs is uniformly_distributed  means :Def11: :: DIST_1:def 11
 for n being Nat st n in dom (FDprobSEQ s) holds
(FDprobSEQ s) . n = 1 / (card S);
end;

:: deftheorem Def11 defines uniformly_distributed DIST_1:def_11_:_
 for S being finite set
for s being FinSequence of S holds
( s is uniformly_distributed iff for n being Nat st n in dom (FDprobSEQ s) holds
(FDprobSEQ s) . n = 1 / (card S) );

theorem Th23: :: DIST_1:21
for S being finite set
for s being FinSequence of S st s is uniformly_distributed holds
FDprobSEQ s is constant
proof
let S be finite set ; ::_thesis: for s being FinSequence of S st s is uniformly_distributed holds
FDprobSEQ s is constant
let s be FinSequence of S; ::_thesis: ( s is uniformly_distributed implies FDprobSEQ s is constant )
assume A1: s is uniformly_distributed ; ::_thesis: FDprobSEQ s is constant
let a, b be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not a in whole_event or not b in whole_event or (FDprobSEQ s) . a = (FDprobSEQ s) . b )
assume that
A2: a in dom (FDprobSEQ s) and
A3: b in dom (FDprobSEQ s) ; ::_thesis: (FDprobSEQ s) . a = (FDprobSEQ s) . b
reconsider na = a, nb = b as Nat by A2, A3;
(FDprobSEQ s) . na = 1 / (card S) by A1, A2, Def11
.= (FDprobSEQ s) . nb by A1, A3, Def11 ;
hence  (FDprobSEQ s) . a = (FDprobSEQ s) . b ; ::_thesis: verum
end;

theorem Th24: :: DIST_1:22
for S being finite set
for s, t being FinSequence of S st s is uniformly_distributed & s,t -are_prob_equivalent holds
t is uniformly_distributed
proof
let S be finite set ; ::_thesis: for s, t being FinSequence of S st s is uniformly_distributed & s,t -are_prob_equivalent holds
t is uniformly_distributed
let s, t be FinSequence of S; ::_thesis: ( s is uniformly_distributed & s,t -are_prob_equivalent implies t is uniformly_distributed )
assume that
A1: s is uniformly_distributed and
A2: s,t -are_prob_equivalent ; ::_thesis: t is uniformly_distributed
 FDprobSEQ s = FDprobSEQ t by A2, Th10;
then  for n being Nat st n in dom (FDprobSEQ t) holds
(FDprobSEQ t) . n = 1 / (card S) by A1, Def11;
hence  t is uniformly_distributed by Def11; ::_thesis: verum
end;

theorem Th25: :: DIST_1:23
for S being finite set
for s, t being FinSequence of S st s is uniformly_distributed & t is uniformly_distributed holds
s,t -are_prob_equivalent
proof
let S be finite set ; ::_thesis: for s, t being FinSequence of S st s is uniformly_distributed & t is uniformly_distributed holds
s,t -are_prob_equivalent
let s, t be FinSequence of S; ::_thesis: ( s is uniformly_distributed & t is uniformly_distributed implies s,t -are_prob_equivalent )
assume that
A1: s is uniformly_distributed and
A2: t is uniformly_distributed ; ::_thesis: s,t -are_prob_equivalent
A3: ( dom (FDprobSEQ s) = Seg (card S) & dom (FDprobSEQ t) = Seg (card S) ) by Def3;
 for n being set st n in dom (FDprobSEQ s) holds
(FDprobSEQ s) . n = (FDprobSEQ t) . n
proof
let n be set ; ::_thesis: ( n in dom (FDprobSEQ s) implies (FDprobSEQ s) . n = (FDprobSEQ t) . n )
assume A4: n in dom (FDprobSEQ s) ; ::_thesis: (FDprobSEQ s) . n = (FDprobSEQ t) . n
then  (FDprobSEQ s) . n = 1 / (card S) by A1, Def11;
hence  (FDprobSEQ s) . n = (FDprobSEQ t) . n by A2, A3, A4, Def11; ::_thesis: verum
end;
then  FDprobSEQ s = FDprobSEQ t by A3, FUNCT_1:2;
hence  s,t -are_prob_equivalent by Th10; ::_thesis: verum
end;

registration
let S be finite set ;
cluster canFS S ->  uniformly_distributed ;
coherence
 canFS S is uniformly_distributed
proof
set s = canFS S;
A1: len (canFS S) = card S by UPROOTS:3;
then  dom (canFS S) = Seg (card S) by FINSEQ_1:def_3;
then A2: dom (canFS S) = dom (FDprobSEQ (canFS S)) by Def3;
 for n being Nat st n in dom (canFS S) holds
(FDprobSEQ (canFS S)) . n = 1 / (card S)
proof
let n be Nat; ::_thesis: ( n in dom (canFS S) implies (FDprobSEQ (canFS S)) . n = 1 / (card S) )
assume A3: n in dom (canFS S) ; ::_thesis: (FDprobSEQ (canFS S)) . n = 1 / (card S)
then (FDprobSEQ (canFS S)) . n = FDprobability (((canFS S) . n),(canFS S)) by A2, Def3
.= (card {n}) / (len (canFS S)) by A3, FINSEQ_5:4
.= 1 / (card S) by A1, CARD_1:30 ;
hence  (FDprobSEQ (canFS S)) . n = 1 / (card S) ; ::_thesis: verum
end;
hence  canFS S is uniformly_distributed by A2, Def11; ::_thesis: verum
end;
end;

Lm2:  for S being finite set
for s being FinSequence of S st s in Finseq-EQclass (canFS S) holds
s is uniformly_distributed
proof
let S be finite set ; ::_thesis: for s being FinSequence of S st s in Finseq-EQclass (canFS S) holds
s is uniformly_distributed
let s be FinSequence of S; ::_thesis: ( s in Finseq-EQclass (canFS S) implies s is uniformly_distributed )
assume  s in Finseq-EQclass (canFS S) ; ::_thesis: s is uniformly_distributed
then  s, canFS S -are_prob_equivalent by Th7;
hence  s is uniformly_distributed by Th24; ::_thesis: verum
end;

Lm3:  for S being finite set
for s being FinSequence of S st s is uniformly_distributed holds
for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass s
proof
let S be finite set ; ::_thesis: for s being FinSequence of S st s is uniformly_distributed holds
for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass s
let s be FinSequence of S; ::_thesis: ( s is uniformly_distributed implies for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass s )
assume A1: s is uniformly_distributed ; ::_thesis: for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass s
let t be FinSequence of S; ::_thesis: ( t is uniformly_distributed implies t in Finseq-EQclass s )
assume  t is uniformly_distributed ; ::_thesis: t in Finseq-EQclass s
then  s,t -are_prob_equivalent by A1, Th25;
hence  t in Finseq-EQclass s ; ::_thesis: verum
end;

definition
let S be finite set ;
func uniform_distribution S ->  Element of distribution_family S means :Def12: :: DIST_1:def 12
 for s being FinSequence of S holds
( s in it iff s is uniformly_distributed );
existence
 ex b1 being Element of distribution_family S st
for s being FinSequence of S holds
( s in b1 iff s is uniformly_distributed )
proof
set s = canFS S;
consider CS being non empty Subset of (S *) such that
A2: CS = Finseq-EQclass (canFS S) ;
reconsider CS = CS as Element of distribution_family S by A2, Def6;
take  CS ; ::_thesis: for s being FinSequence of S holds
( s in CS iff s is uniformly_distributed )
 for t being FinSequence of S st t in CS holds
canFS S,t -are_prob_equivalent by A2, Th7;
then  for t being FinSequence of S st t in CS holds
t is uniformly_distributed by Th24;
hence  for s being FinSequence of S holds
( s in CS iff s is uniformly_distributed ) by A2, Lm3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of distribution_family S st ( for s being FinSequence of S holds
( s in b1 iff s is uniformly_distributed ) ) & ( for s being FinSequence of S holds
( s in b2 iff s is uniformly_distributed ) ) holds
b1 = b2
proof
let A, B be Element of distribution_family S; ::_thesis: ( ( for s being FinSequence of S holds
( s in A iff s is uniformly_distributed ) ) & ( for s being FinSequence of S holds
( s in B iff s is uniformly_distributed ) ) implies A = B )
assume A4: for s being FinSequence of S holds
( s in A iff s is uniformly_distributed ) ; ::_thesis: ( ex s being FinSequence of S st
( ( s in B implies s is uniformly_distributed ) implies ( s is uniformly_distributed & not s in B ) ) or A = B )
assume A5: for s being FinSequence of S holds
( s in B iff s is uniformly_distributed ) ; ::_thesis: A = B
A6: for s being set st s in B holds
s in A
proof
let s be set ; ::_thesis: ( s in B implies s in A )
assume A7: s in B ; ::_thesis: s in A
then reconsider s = s as Element of S * ;
 s is uniformly_distributed by A5, A7;
hence  s in A by A4; ::_thesis: verum
end;
 for s being set st s in A holds
s in B
proof
let s be set ; ::_thesis: ( s in A implies s in B )
assume A8: s in A ; ::_thesis: s in B
then reconsider s = s as Element of S * ;
 s is uniformly_distributed by A4, A8;
hence  s in B by A5; ::_thesis: verum
end;
hence  A = B by A6, TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines uniform_distribution DIST_1:def_12_:_
 for S being finite set
for b2 being Element of distribution_family S holds
( b2 = uniform_distribution S iff for s being FinSequence of S holds
( s in b2 iff s is uniformly_distributed ) );

registration
let S be non empty finite set ;
cluster non empty Relation-like NAT -defined REAL -valued Function-like constant finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS for distProbFinS of S;
existence
 ex b1 being distProbFinS of S st b1 is constant
proof
reconsider s = canFS S as Element of S * by FINSEQ_1:def_11;
take p = FDprobSEQ s; ::_thesis: ( p is distProbFinS of S & p is constant )
 dom p = Seg (card S) by Def3;
then  len p = card S by FINSEQ_1:def_3;
hence  ( p is distProbFinS of S & p is constant ) by Def10, Th23; ::_thesis: verum
end;
end;

definition
let S be non empty finite set ;
func Uniform_FDprobSEQ S ->  distProbFinS of S equals :: DIST_1:def 13
 FDprobSEQ (canFS S);
coherence
 FDprobSEQ (canFS S) is distProbFinS of S
proof
reconsider s = canFS S as Element of S * by FINSEQ_1:def_11;
set p = FDprobSEQ s;
 dom (FDprobSEQ s) = Seg (card S) by Def3;
then  len (FDprobSEQ s) = card S by FINSEQ_1:def_3;
hence  FDprobSEQ (canFS S) is distProbFinS of S by Def10; ::_thesis: verum
end;
end;

:: deftheorem  defines Uniform_FDprobSEQ DIST_1:def_13_:_
 for S being non empty finite set holds Uniform_FDprobSEQ S = FDprobSEQ (canFS S);

registration
let S be non empty finite set ;
cluster Uniform_FDprobSEQ S ->  constant ;
coherence
 Uniform_FDprobSEQ S is constant by Th23;
end;

theorem :: DIST_1:24
for S being non empty finite set holds uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S)
proof
let S be non empty finite set ; ::_thesis: uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S)
set p = Uniform_FDprobSEQ S;
set s = canFS S;
A2: for t being FinSequence of S st t is uniformly_distributed holds
t in Finseq-EQclass (canFS S)
proof
let t be FinSequence of S; ::_thesis: ( t is uniformly_distributed implies t in Finseq-EQclass (canFS S) )
assume  t is uniformly_distributed ; ::_thesis: t in Finseq-EQclass (canFS S)
then  canFS S,t -are_prob_equivalent by Th25;
hence  t in Finseq-EQclass (canFS S) ; ::_thesis: verum
end;
 ( ( for t being FinSequence of S st t in Finseq-EQclass (canFS S) holds
t is uniformly_distributed ) & Finseq-EQclass (canFS S) is Element of distribution_family S ) by Def6, Lm2;
then A3: Finseq-EQclass (canFS S) = uniform_distribution S by A2, Def12;
 (GenProbSEQ S) . (Finseq-EQclass (canFS S)) = Uniform_FDprobSEQ S by Th12;
then A4: (GenProbSEQ S) . (distribution ((Uniform_FDprobSEQ S),S)) = (GenProbSEQ S) . (Finseq-EQclass (canFS S)) by Th22;
 dom (GenProbSEQ S) = distribution_family S by FUNCT_2:def_1;
hence  uniform_distribution S = distribution ((Uniform_FDprobSEQ S),S) by A3, A4, FUNCT_1:def_4; ::_thesis: verum
end;