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
( () . n = frequency (x,s) & x = () . 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
( () . n = frequency (x,s) & x = () . n )

let n be Nat; :: thesis: ( n in Seg (card S) implies ex x being Element of S st
( () . n = frequency (x,s) & x = () . n ) )

set y = (len s) * (() . n);
A1: rng () = S by FUNCT_2:def 3;
assume A2: n in Seg (card S) ; :: thesis: ex x being Element of S st
( () . n = frequency (x,s) & x = () . n )

then A3: n in dom () by Def9;
Seg (len ()) = Seg (card S) by FINSEQ_1:93;
then n in dom () by ;
then (canFS S) . n is Element of S by ;
then consider a being Element of S such that
A4: a = () . n ;
take a ; :: thesis: ( () . n = frequency (a,s) & a = () . n )
n in dom () by ;
then (len s) * (() . n) = (len s) * (FDprobability (a,s)) by ;
then (len s) * (() . n) = frequency (a,s) by XCMPLX_1:87;
hence ( (freqSEQ s) . n = frequency (a,s) & a = () . n ) by A3, A4, Def9; :: thesis: verum