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

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