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 PP0: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
PP1: for x, y1, y2 being set st x in dom (freqSEQ s) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
PP2: 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] )
assume x in dom (freqSEQ s) ; :: thesis: ex y being set st S₁[x,y]
then LPP22P: x in Seg (card S) by defDIST;
set z = (canFS S) . x;
rng (canFS S) = S by FUNCT_2:def 3;
then reconsider z = (canFS S) . x as Element of S by FUNCT_1:12, LPP22P, PP0;
consider y being set such that
LPP25: y = s " {z} ;
LPP26: y = event_pick z,s by LPP25;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by LPP26; :: thesis: verum

end;

consider T being Function such that
P1: ( 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(PP1, PP2);
LMISS1: 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 ZTA: ( a in dom T & b in dom T & a <> b ) ; :: thesis: T . a misses T . b
ZT1: ( a in dom (canFS S) & b in dom (canFS S) ) by P1, ZTA, PP0, defDIST;
ZT2: (canFS S) . a <> (canFS S) . b by ZTA, FUNCT_1:def 8, ZT1;
consider za being Element of S such that
ZT3: ( za = (canFS S) . a & T . a = event_pick za,s ) by P1, ZTA;
consider zb being Element of S such that
ZT4: ( zb = (canFS S) . b & T . b = event_pick zb,s ) by P1, ZTA;
thus T . a misses T . b by ZT3, ZT4, FUNCT_1:141, ZFMISC_1:17, ZT2; :: 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 ANB: 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 LMISS1, ANB; :: 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 Q1: T is disjoint_valued by PROB_2:def 3;
Q3: 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 ASQ3: i in dom T ; :: thesis: ( T . i is finite & (freqSEQ s) . i = card (T . i) )
then consider zi being Element of S such that
Q3C1: ( zi = (canFS S) . i & T . i = event_pick zi,s ) by P1;
Q3C3: dom (freqSEQ s) = Seg (card S) by defDIST;
Q3C4: i in dom (FDprobSEQ s) by P1, ASQ3, Q3C3, defFREQDIST;
(freqSEQ s) . i = (len s) * ((FDprobSEQ s) . i) by defDIST, ASQ3, P1
.= (len s) * (FDprobability ((canFS S) . i),s) by Q3C4, defFREQDIST
.= card (T . i) by Q3C1, XCMPLX_1:88 ;
hence ( T . i is finite & (freqSEQ s) . i = card (T . i) ) ; :: thesis: verum

end;

reconsider T1 = union (rng T) as finite set by Q1, P1, Q3, LMCARD;
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
RNGT1: ( j in dom T & X = T . j ) by FUNCT_1:def 5;
consider zj being Element of S such that
RNGT2: ( zj = (canFS S) . j & T . j = event_pick zj,s ) by P1, RNGT1;
X c= whole_event s by RNGT1, RNGT2;
hence X c= Seg (len s) by FINSEQ_1:def 3; :: thesis: verum

end;

then L1: union (rng T) c= Seg (len s) by ZFMISC_1:94;
Seg (len s) c= union (rng T)

proof

assume CNTRSEGLS: not Seg (len s) c= union (rng T) ; :: thesis: contradiction
consider ne being set such that
SEGLS1: ( ne in Seg (len s) & not ne in union (rng T) ) by TARSKI:def 3, CNTRSEGLS;
SEGLS2: ne in dom s by SEGLS1, FINSEQ_1:def 3;
set yne = s . ne;
SEGLS4: s . ne in rng s by SEGLS2, FUNCT_1:def 5;
reconsider yne = s . ne as Element of S by SEGLS4;
rng (canFS S) = S by FUNCT_2:def 3;
then consider nne being set such that
SEGLS6: ( nne in dom (canFS S) & yne = (canFS S) . nne ) by FUNCT_1:def 5;
NINDOML: nne in dom (freqSEQ s) by defDIST, PP0, SEGLS6;
then consider zne being Element of S such that
SEGLS7: ( zne = (canFS S) . nne & T . nne = event_pick zne,s ) by P1;
s . ne in {(s . ne)} by TARSKI:def 1;
then SEGLS9: ne in T . nne by SEGLS7, SEGLS6, FUNCT_1:def 13, SEGLS2;
T . nne in rng T by FUNCT_1:12, NINDOML, P1;
hence contradiction by SEGLS1, TARSKI:def 4, SEGLS9; :: thesis: verum

end;

then Q5: T1 = Seg (len s) by L1, XBOOLE_0:def 10;
thus Sum (freqSEQ s) = card T1 by Q1, P1, Q3, LMCARD
.= len s by FINSEQ_1:78, Q5 ; :: thesis: verum