let S be non empty finite set ; :: thesis: for s being non empty FinSequence of S
for n being Nat st n in Seg (card S) holds
ex x being Element of S st
( (freqSEQ s) . n = frequency x,s & x = (canFS S) . n )
let s be non empty FinSequence of S; :: thesis: for n being Nat st n in Seg (card S) holds
ex x being Element of S st
( (freqSEQ s) . n = frequency x,s & x = (canFS S) . n )
let n be Nat; :: thesis: ( n in Seg (card S) implies ex x being Element of S st
( (freqSEQ s) . n = frequency x,s & x = (canFS S) . n ) )
assume SAS1: n in Seg (card S) ; :: thesis: ex x being Element of S st
( (freqSEQ s) . n = frequency x,s & x = (canFS S) . n )
SAS2: ( n in dom (freqSEQ s) & n in dom (FDprobSEQ s) ) by defDIST, defFREQDIST, SAS1;
consider y being Real such that
SAS4: y = (len s) * ((FDprobSEQ s) . n) ;
Seg (len (canFS S)) = Seg (card S) by UPROOTS:5;
then SAS5: n in dom (canFS S) by SAS1, FINSEQ_1:def 3;
rng (canFS S) = S by FUNCT_2:def 3;
then (canFS S) . n is Element of S by SAS5, FUNCT_1:12;
then consider a being Element of S such that
SAS7: a = (canFS S) . n ;
SAS8: y = (len s) * (FDprobability a,s) by SAS2, defFREQDIST, SAS4, SAS7;
T2: y = frequency a,s by SAS8, XCMPLX_1:88;
take a ; :: thesis: ( (freqSEQ s) . n = frequency a,s & a = (canFS S) . n )
thus ( (freqSEQ s) . n = frequency a,s & a = (canFS S) . n ) by SAS2, T2, SAS7, defDIST, SAS4; :: thesis: verum