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 S_{1}[ object , object ] means ex z being Element of S st

( z = (canFS S) . $1 & $2 = event_pick (z,s) );

len (canFS S) = card S by FINSEQ_1:93;

then A1: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;

A2: for x being object st x in dom (freqSEQ s) holds

ex y being object st S_{1}[x,y]

A4: ( dom T = dom (freqSEQ s) & ( for x being object st x in dom (freqSEQ s) holds

S_{1}[x,T . x] ) )
from CLASSES1:sch 1(A2);

A5: for a, b being set st a in dom T & b in dom T & a <> b holds

T . a misses T . b

T . a misses T . b

A11: Seg (len s) c= Union T

( T . i is finite & (freqSEQ s) . i = card (T . i) )

for X being set st X in rng T holds

X c= Seg (len s)

then A26: T1 = Seg (len s) by A11;

thus Sum (freqSEQ s) = card T1 by A4, A10, A20, Th15

.= len s by A26, FINSEQ_1:57 ; :: thesis: verum

let s be non empty FinSequence of S; :: thesis: Sum (freqSEQ s) = len s

set L = freqSEQ s;

defpred S

( z = (canFS S) . $1 & $2 = event_pick (z,s) );

len (canFS S) = card S by FINSEQ_1:93;

then A1: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;

A2: for x being object st x in dom (freqSEQ s) holds

ex y being object st S

proof

consider T being Function such that
let x be object ; :: thesis: ( x in dom (freqSEQ s) implies ex y being object st S_{1}[x,y] )

set z = (canFS S) . x;

assume x in dom (freqSEQ s) ; :: thesis: ex y being object st S_{1}[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: S_{1}[x,s " {z}]

s " {z} = event_pick (z,s) ;

hence S_{1}[x,s " {z}]
; :: thesis: verum

end;set z = (canFS S) . x;

assume x in dom (freqSEQ s) ; :: thesis: ex y being object st S

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

s " {z} = event_pick (z,s) ;

hence S

A4: ( dom T = dom (freqSEQ s) & ( for x being object st x in dom (freqSEQ s) holds

S

A5: for a, b being set st a in dom T & b in dom T & a <> b holds

T . a misses T . b

proof

for a, b being object st a <> b holds
let a, b be set ; :: thesis: ( a in dom T & b in dom T & a <> b implies T . a misses T . b )

assume that

A6: ( a in dom T & b in dom T ) and

A7: a <> b ; :: thesis: T . a misses T . b

( a in dom (canFS S) & b in dom (canFS S) ) by A1, A4, A6, Def9;

then A8: (canFS S) . a <> (canFS S) . b by A7, 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 A4, A6;

hence T . a misses T . b by A8, FUNCT_1:71, ZFMISC_1:11; :: thesis: verum

end;assume that

A6: ( a in dom T & b in dom T ) and

A7: a <> b ; :: thesis: T . a misses T . b

( a in dom (canFS S) & b in dom (canFS S) ) by A1, A4, A6, Def9;

then A8: (canFS S) . a <> (canFS S) . b by A7, 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 A4, A6;

hence T . a misses T . b by A8, FUNCT_1:71, ZFMISC_1:11; :: thesis: verum

T . a misses T . b

proof

then A10:
T is disjoint_valued
by PROB_2:def 2;
let a, b be object ; :: thesis: ( a <> b implies T . a misses T . b )

assume A9: a <> b ; :: thesis: T . a misses T . b

end;assume A9: a <> b ; :: thesis: T . a misses T . b

A11: Seg (len s) c= Union T

proof

A20:
for i being Nat st i in dom T holds
assume
not Seg (len s) c= Union T
; :: thesis: contradiction

then consider ne being object such that

A12: ne in Seg (len s) and

A13: not ne in Union T ;

set yne = s . ne;

A14: ne in dom s by A12, 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 object such that

A15: nne in dom (canFS S) and

A16: yne = (canFS S) . nne by FUNCT_1:def 3;

A17: nne in dom (freqSEQ s) by A1, A15, Def9;

then A18: T . nne in rng T by A4, FUNCT_1:3;

A19: 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 A4, A17;

then ne in T . nne by A14, A16, A19, FUNCT_1:def 7;

hence contradiction by A13, A18, TARSKI:def 4; :: thesis: verum

end;then consider ne being object such that

A12: ne in Seg (len s) and

A13: not ne in Union T ;

set yne = s . ne;

A14: ne in dom s by A12, 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 object such that

A15: nne in dom (canFS S) and

A16: yne = (canFS S) . nne by FUNCT_1:def 3;

A17: nne in dom (freqSEQ s) by A1, A15, Def9;

then A18: T . nne in rng T by A4, FUNCT_1:3;

A19: 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 A4, A17;

then ne in T . nne by A14, A16, A19, FUNCT_1:def 7;

hence contradiction by A13, A18, TARSKI:def 4; :: thesis: verum

( T . i is finite & (freqSEQ s) . i = card (T . i) )

proof

then reconsider T1 = Union T as finite set by A4, A10, Th15;
let i be Nat; :: thesis: ( i in dom T implies ( T . i is finite & (freqSEQ s) . i = card (T . i) ) )

assume A21: i in dom T ; :: thesis: ( T . i is finite & (freqSEQ s) . i = card (T . i) )

then A22: ex zi being Element of S st

( zi = (canFS S) . i & T . i = event_pick (zi,s) ) by A4;

dom (freqSEQ s) = Seg (card S) by Def9;

then A23: i in dom (FDprobSEQ s) by A4, A21, Def3;

(freqSEQ s) . i = (len s) * ((FDprobSEQ s) . i) by A4, A21, Def9

.= (len s) * (FDprobability (((canFS S) . i),s)) by A23, Def3

.= card (T . i) by A22, XCMPLX_1:87 ;

hence ( T . i is finite & (freqSEQ s) . i = card (T . i) ) ; :: thesis: verum

end;assume A21: i in dom T ; :: thesis: ( T . i is finite & (freqSEQ s) . i = card (T . i) )

then A22: ex zi being Element of S st

( zi = (canFS S) . i & T . i = event_pick (zi,s) ) by A4;

dom (freqSEQ s) = Seg (card S) by Def9;

then A23: i in dom (FDprobSEQ s) by A4, A21, Def3;

(freqSEQ s) . i = (len s) * ((FDprobSEQ s) . i) by A4, A21, Def9

.= (len s) * (FDprobability (((canFS S) . i),s)) by A23, Def3

.= card (T . i) by A22, XCMPLX_1:87 ;

hence ( T . i is finite & (freqSEQ s) . i = card (T . i) ) ; :: thesis: verum

for X being set st X in rng T holds

X c= Seg (len s)

proof

then
Union T c= Seg (len s)
by ZFMISC_1:76;
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 object such that

A24: j in dom T and

A25: 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 A4, A24;

then X c= whole_event by A25;

hence X c= Seg (len s) by FINSEQ_1:def 3; :: thesis: verum

end;assume X in rng T ; :: thesis: X c= Seg (len s)

then consider j being object such that

A24: j in dom T and

A25: 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 A4, A24;

then X c= whole_event by A25;

hence X c= Seg (len s) by FINSEQ_1:def 3; :: thesis: verum

then A26: T1 = Seg (len s) by A11;

thus Sum (freqSEQ s) = card T1 by A4, A10, A20, Th15

.= len s by A26, FINSEQ_1:57 ; :: thesis: verum