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