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₁[ 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:5;
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 S₁[x,y]

proof

let x be set ; :: thesis: ( x in dom (freqSEQ s) implies ex y being set st S₁[x,y] )
set z = (canFS S) . x;
assume x in dom (freqSEQ s) ; :: thesis: ex y being set st S₁[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:12;
consider y being set such that
A4: y = s " {z} ;
take y ; :: thesis: S₁[x,y]
y = event_pick (z,s) by A4;
hence S₁[x,y] ; :: thesis: verum

end;

A5: for x, y1, y2 being set st x in dom (freqSEQ s) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
consider T being Function such that
A6: ( dom T = dom (freqSEQ s) & ( for x being set st x in dom (freqSEQ s) holds
S₁[x,T . x] ) ) from FUNCT_1:sch 2(A5, A2);
A7: 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
A8: ( a in dom T & b in dom T ) and
A9: a <> b ; :: thesis: T . a misses T . b
( a in dom (canFS S) & b in dom (canFS S) ) by A1, A6, A8, Def9;
then A10: (canFS S) . a <> (canFS S) . b by A9, FUNCT_1:def 8;
( 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 A6, A8;
hence T . a misses T . b by A10, FUNCT_1:141, ZFMISC_1:17; :: 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 A11: a <> b ; :: thesis: T . a misses T . b

now

per cases ( ( a in dom T & b in dom T ) or not a in dom T or ( a in dom T & not b in dom T ) ) ;

case ( a in dom T & b in dom T ) ; :: thesis: T . a misses T . b

hence T . a misses T . b by A7, A11; :: thesis: verum

end;

case not a in dom T ; :: thesis: T . a misses T . b

then T . a = {} by FUNCT_1:def 4;
hence T . a misses T . b by XBOOLE_1:65; :: thesis: verum

end;

case ( a in dom T & not b in dom T ) ; :: thesis: T . a misses T . b

then T . b = {} by FUNCT_1:def 4;
hence T . a misses T . b by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence T . a misses T . b ; :: thesis: verum

end;

then A12: T is disjoint_valued by PROB_2:def 3;
A13: Seg (len s) c= union (rng T)

proof

assume not Seg (len s) c= union (rng T) ; :: thesis: contradiction
then consider ne being set such that
A14: ne in Seg (len s) and
A15: not ne in union (rng T) by TARSKI:def 3;
set yne = s . ne;
A16: ne in dom s by A14, FINSEQ_1:def 3;
then s . ne in rng s by FUNCT_1:def 5;
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
A17: nne in dom (canFS S) and
A18: yne = (canFS S) . nne by FUNCT_1:def 5;
A19: nne in dom (freqSEQ s) by A1, A17, Def9;
then A20: T . nne in rng T by A6, FUNCT_1:12;
A21: 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 A6, A19;
then ne in T . nne by A16, A18, A21, FUNCT_1:def 13;
hence contradiction by A15, A20, TARSKI:def 4; :: thesis: verum

end;

A22: 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 A23: i in dom T ; :: thesis: ( T . i is finite & (freqSEQ s) . i = card (T . i) )
then A24: ex zi being Element of S st
( zi = (canFS S) . i & T . i = event_pick (zi,s) ) by A6;
dom (freqSEQ s) = Seg (card S) by Def9;
then A25: i in dom (FDprobSEQ s) by A6, A23, Def3;
(freqSEQ s) . i = (len s) * ((FDprobSEQ s) . i) by A6, A23, Def9
.= (len s) * (FDprobability (((canFS S) . i),s)) by A25, Def3
.= card (T . i) by A24, XCMPLX_1:88 ;
hence ( T . i is finite & (freqSEQ s) . i = card (T . i) ) ; :: thesis: verum

end;

then reconsider T1 = union (rng T) as finite set by A6, A12, 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
A26: j in dom T and
A27: X = T . j by FUNCT_1:def 5;
ex zj being Element of S st
( zj = (canFS S) . j & T . j = event_pick (zj,s) ) by A6, A26;
then X c= whole_event by A27;
hence X c= Seg (len s) by FINSEQ_1:def 3; :: thesis: verum

end;

then union (rng T) c= Seg (len s) by ZFMISC_1:94;
then A28: T1 = Seg (len s) by A13, XBOOLE_0:def 10;
thus Sum (freqSEQ s) = card T1 by A6, A12, A22, Th18
.= len s by A28, FINSEQ_1:78 ; :: thesis: verum