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 ) )
consider y being Real such that
A1: y = (len s) * ((FDprobSEQ s) . n) ;
A2: rng (canFS S) = S by FUNCT_2:def 3;
assume A3: n in Seg (card S) ; :: thesis: ex x being Element of S st
( (freqSEQ s) . n = frequency x,s & x = (canFS S) . n )
then A4: n in dom (freqSEQ s) by Def9;
Seg (len (canFS S)) = Seg (card S) by UPROOTS:5;
then n in dom (canFS S) by A3, FINSEQ_1:def 3;
then (canFS S) . n is Element of S by A2, FUNCT_1:12;
then consider a being Element of S such that
A5: a = (canFS S) . n ;
take a ; :: thesis: ( (freqSEQ s) . n = frequency a,s & a = (canFS S) . n )
n in dom (FDprobSEQ s) by A3, Def3;
then y = (len s) * (FDprobability a,s) by A1, A5, Def3;
then y = frequency a,s by XCMPLX_1:88;
hence ( (freqSEQ s) . n = frequency a,s & a = (canFS S) . n ) by A4, A1, A5, Def9; :: thesis: verum