let S be non empty finite set ; :: thesis: for s being non empty FinSequence of S holds Sum () = len s
let s be non empty FinSequence of S; :: thesis: Sum () = len s
set L = freqSEQ s;
defpred S1[ object , object ] means ex z being Element of S st
( z = () . \$1 & \$2 = event_pick (z,s) );
len () = card S by FINSEQ_1:93;
then A1: dom () = Seg (card S) by FINSEQ_1:def 3;
A2: for x being object st x in dom () holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in dom () implies ex y being object st S1[x,y] )
set z = () . x;
assume x in dom () ; :: thesis: ex y being object st S1[x,y]
then A3: x in Seg (card S) by Def9;
rng () = S by FUNCT_2:def 3;
then reconsider z = () . x as Element of S by ;
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
A4: ( dom T = dom () & ( for x being object st x in dom () holds
S1[x,T . x] ) ) from 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 () & b in dom () ) by A1, A4, A6, Def9;
then A8: (canFS S) . a <> () . b by ;
( ex za being Element of S st
( za = () . a & T . a = event_pick (za,s) ) & ex zb being Element of S st
( zb = () . b & T . b = event_pick (zb,s) ) ) by A4, A6;
hence T . a misses T . b by ; :: 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 ( a in dom T & not b in dom T ) ; :: thesis: T . a misses T . b
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 ;
then s . ne in rng s by FUNCT_1:def 3;
then reconsider yne = s . ne as Element of S ;
rng () = S by FUNCT_2:def 3;
then consider nne being object such that
A15: nne in dom () and
A16: yne = () . nne by FUNCT_1:def 3;
A17: nne in dom () by ;
then A18: T . nne in rng T by ;
A19: s . ne in {(s . ne)} by TARSKI:def 1;
ex zne being Element of S st
( zne = () . nne & T . nne = event_pick (zne,s) ) by ;
then ne in T . nne by ;
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 & () . i = card (T . i) )
proof
let i be Nat; :: thesis: ( i in dom T implies ( T . i is finite & () . i = card (T . i) ) )
assume A21: i in dom T ; :: thesis: ( T . i is finite & () . i = card (T . i) )
then A22: ex zi being Element of S st
( zi = () . i & T . i = event_pick (zi,s) ) by A4;
dom () = Seg (card S) by Def9;
then A23: i in dom () by ;
() . i = (len s) * (() . i) by
.= (len s) * (FDprobability ((() . i),s)) by
.= card (T . i) by ;
hence ( T . i is finite & () . i = card (T . i) ) ; :: thesis: verum
end;
then reconsider T1 = Union T as finite set by ;
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 = () . j & T . j = event_pick (zj,s) ) by ;
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 () = card T1 by A4, A10, A20, Th15
.= len s by ; :: thesis: verum