let S be non empty finite set ; :: thesis:
let D be EqSampleSpaces of S; :: thesis:
let s be Element of D; :: thesis:
let judgefunc be Function of S,BOOLEAN; :: thesis:
len (canFS S) = card S by FINSEQ_1:93;
then A1: dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
A2: trueEVENT (judgefunc * (canFS S)) is Event of (dom (canFS S)) by Th8;
reconsider A = trueEVENT (judgefunc * (canFS S)) as Subset of (dom (freqSEQ s)) by A1, A2, DIST_1:def 9;
A3: len (extract ((freqSEQ s),A)) = card A by Th11;
set L = extract ((freqSEQ s),A);
A4: dom (extract ((freqSEQ s),A)) = Seg (card A) by A3, FINSEQ_1:def 3;
defpred S₁[ object , object ] means ex z being Element of S st
( z = (canFS S) . ((canFS A) . $1) & $2 = event_pick (z,s) );
len (canFS A) = card A by FINSEQ_1:93;
then A5: dom (canFS A) = Seg (card A) by FINSEQ_1:def 3;
A6: for x, y1, y2 being object st x in dom (extract ((freqSEQ s),A)) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A7: for x being object st x in dom (extract ((freqSEQ s),A)) holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis:
assume x in dom (extract ((freqSEQ s),A)) ; :: thesis:
then A8: x in Seg (card A) by A3, FINSEQ_1:def 3;
set z = (canFS S) . ((canFS A) . x);
rng (canFS A) = A by FUNCT_2:def 3;
then A9: (canFS A) . x in A by A5, A8, FUNCT_1:3;
rng (canFS S) = S by FUNCT_2:def 3;
then reconsider z = (canFS S) . ((canFS A) . x) as Element of S by A9, A2, FUNCT_1:3;
set y = s " {z};
A10: s " {z} = event_pick (z,s) ;
take s " {z} ; :: thesis:
thus S₁[x,s " {z}] by A10; :: thesis:

end;

consider G being Function such that
A11: ( dom G = dom (extract ((freqSEQ s),A)) & ( for x being object st x in dom (extract ((freqSEQ s),A)) holds
S₁[x,G . x] ) ) from FUNCT_1:sch 2(A6, A7);
A12: for a, b being set st a in dom G & b in dom G & a <> b holds
G . a misses G . b

proof

let a, b be set ; :: thesis:
assume A13: ( a in dom G & b in dom G & a <> b ) ; :: thesis:
then A14: ( a in dom (canFS A) & b in dom (canFS A) ) by A3, A5, A11, FINSEQ_1:def 3;
rng (canFS A) = A by FUNCT_2:def 3;
then A15: ( (canFS A) . a in A & (canFS A) . b in A ) by A14, FUNCT_1:3;
(canFS A) . a <> (canFS A) . b by A14, A13, FUNCT_1:def 4;
then A16: (canFS S) . ((canFS A) . a) <> (canFS S) . ((canFS A) . b) by A15, A2, FUNCT_1:def 4;
consider za being Element of S such that
A17: ( za = (canFS S) . ((canFS A) . a) & G . a = event_pick (za,s) ) by A11, A13;
consider zb being Element of S such that
A18: ( zb = (canFS S) . ((canFS A) . b) & G . b = event_pick (zb,s) ) by A11, A13;
thus G . a misses G . b by A17, A18, A16, FUNCT_1:71, ZFMISC_1:11; :: thesis:

end;

A19: for i being Nat st i in dom G holds
( G . i is finite & (extract ((freqSEQ s),A)) . i = card (G . i) )

proof

let i be Nat; :: thesis:
assume A20: i in dom G ; :: thesis:
then consider zi being Element of S such that
A21: ( zi = (canFS S) . ((canFS A) . i) & G . i = event_pick (zi,s) ) by A11;
A22: i in dom (canFS A) by A3, A5, A11, A20, FINSEQ_1:def 3;
rng (canFS A) = A by FUNCT_2:def 3;
then A23: (canFS A) . i in A by A22, FUNCT_1:3;
then A24: (canFS A) . i in Seg (card S) by A2, A1;
A25: (canFS A) . i in dom (FDprobSEQ s) by A24, DIST_1:def 3;
(extract ((freqSEQ s),A)) . i = (freqSEQ s) . ((canFS A) . i) by A20, A11, Th11
.= (len s) * ((FDprobSEQ s) . ((canFS A) . i)) by A23, DIST_1:def 9
.= (len s) * (FDprobability (((canFS S) . ((canFS A) . i)),s)) by A25, DIST_1:def 3
.= card (G . i) by A21, XCMPLX_1:87 ;
hence ( G . i is finite & (extract ((freqSEQ s),A)) . i = card (G . i) ) ; :: thesis:

end;

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

proof

let a, b be object ; :: thesis:
assume A26: a <> b ; :: thesis:

per cases ;

suppose ( a in dom G & b in dom G ) ; :: thesis:

hence G . a misses G . b by A12, A26; :: thesis:

end;

suppose not a in dom G ; :: thesis:

then G . a = {} by FUNCT_1:def 2;
hence G . a misses G . b by XBOOLE_1:65; :: thesis:

end;

suppose ( a in dom G & not b in dom G ) ; :: thesis:

then G . b = {} by FUNCT_1:def 2;
hence G . a misses G . b by XBOOLE_1:65; :: thesis:

end;

then A27: G is disjoint_valued by PROB_2:def 2;
for X being set st X in rng G holds
X c= trueEVENT (judgefunc * s)

proof

let X be set ; :: thesis:
assume X in rng G ; :: thesis:
then consider j being object such that
A28: ( j in dom G & X = G . j ) by FUNCT_1:def 3;
consider zj being Element of S such that
A29: ( zj = (canFS S) . ((canFS A) . j) & G . j = event_pick (zj,s) ) by A11, A28;
zj in trueEVENT judgefunc

proof

j in dom (canFS A) by A28, A5, A11, A3, FINSEQ_1:def 3;
then (canFS A) . j in rng (canFS A) by FUNCT_1:3;
then (canFS A) . j in A by FUNCT_2:def 3;
hence zj in trueEVENT judgefunc by Th13, A29, A2; :: thesis:

end;

then for x being object st x in {zj} holds
x in trueEVENT judgefunc by TARSKI:def 1;
then s " {zj} c= s " (trueEVENT judgefunc) by RELAT_1:143, TARSKI:def 3;
hence X c= trueEVENT (judgefunc * s) by A28, A29, Th14; :: thesis:

end;

then A30: union (rng G) c= trueEVENT (judgefunc * s) by ZFMISC_1:76;
for x being object st x in trueEVENT (judgefunc * s) holds
x in union (rng G)

proof

let x be object ; :: thesis:
assume A31: x in trueEVENT (judgefunc * s) ; :: thesis:
A32: trueEVENT (judgefunc * s) is Event of (dom s) by Th8;
reconsider n = x as Nat by A31;
A33: s . n in trueEVENT judgefunc by A32, Th13, A31;
A34: trueEVENT judgefunc c= S

proof

dom judgefunc = S by FUNCT_2:def 1;
hence trueEVENT judgefunc c= S ; :: thesis:

end;

ex m being Nat st
( m in Seg (card S) & s . n = (canFS S) . m )

proof

( s . n in rng (canFS S) & ex m being Nat st
( m in dom (canFS S) & s . n = (canFS S) . m & m in Seg (card S) ) ) by Th3, A34, A33;
hence ex m being Nat st
( m in Seg (card S) & s . n = (canFS S) . m ) ; :: thesis:

end;

then consider m being Nat such that
A35: ( m in Seg (card S) & s . n = (canFS S) . m ) ;
reconsider D0 = uniform_distribution S as EqSampleSpaces of S ;
len (canFS S) = card S by FINSEQ_1:93;
then A36: m in dom (canFS S) by A35, FINSEQ_1:def 3;
A37: m in trueEVENT (judgefunc * (canFS S)) by A36, Th13, A33, A35;
ex k being Nat st
( k in Seg (card A) & m = (canFS A) . k )

proof

reconsider m = m as Element of A by A36, Th13, A33, A35;
( m in rng (canFS A) & ex k being Nat st
( k in dom (canFS A) & m = (canFS A) . k & k in Seg (card A) ) ) by Th3, A37;
hence ex k being Nat st
( k in Seg (card A) & m = (canFS A) . k ) ; :: thesis:

end;

then consider k being Nat such that
A38: ( k in Seg (card A) & m = (canFS A) . k ) ;
s . n in {((canFS S) . ((canFS A) . k))} by A35, A38, TARSKI:def 1;
then A39: n in s " {((canFS S) . ((canFS A) . k))} by A32, A31, FUNCT_1:def 7;
consider z being Element of S such that
A40: ( z = (canFS S) . ((canFS A) . k) & G . k = event_pick (z,s) ) by A38, A11, A4;
dom G = Seg (card A) by A11, A3, FINSEQ_1:def 3;
then G . k c= union (rng G) by A38, FUNCT_1:3, ZFMISC_1:74;
hence x in union (rng G) by A39, A40; :: thesis:

end;

then trueEVENT (judgefunc * s) c= union (rng G) by TARSKI:def 3;
then A41: union (rng G) = trueEVENT (judgefunc * s) by A30, XBOOLE_0:def 10;
card (Union G) = Sum (extract ((freqSEQ s),A)) by A11, A19, A27, DIST_1:17;
hence ex A being Subset of (dom (freqSEQ s)) st
( A = trueEVENT (judgefunc * (canFS S)) & card (trueEVENT (judgefunc * s)) = Sum (extract ((freqSEQ s),A)) ) by A41; :: thesis: