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₁[ 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₁[x,y]

proof

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

end;

consider T being Function such that
A4: ( dom T = dom (freqSEQ s) & ( for x being object st x in dom (freqSEQ s) holds
S₁[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

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

for a, b being object st a <> b holds
T . a misses T . b

proof

let a, b be object ; :: thesis: ( a <> b implies T . a misses T . b )
assume A9: a <> b ; :: thesis: T . a misses T . b

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

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

hence T . a misses T . b by A5, A9; :: 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 ; :: 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 ; :: thesis: verum

end;

end;

end;

then A10: T is disjoint_valued by PROB_2:def 2;
A11: Seg (len s) c= Union T

proof

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;

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

then reconsider T1 = Union T as finite set by A4, A10, Th15;
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 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;

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