:: 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;