let S be non empty finite set ; :: thesis: for D being EqSampleSpaces of S
for s being Element of D holds freqSEQ s = (len s) (#) (FDprobSEQ s)
let D be EqSampleSpaces of S; :: thesis: for s being Element of D holds freqSEQ s = (len s) (#) (FDprobSEQ s)
let s be Element of D; :: thesis: freqSEQ s = (len s) (#) (FDprobSEQ s)
dom (freqSEQ s) = Seg (card S) by DIST_1:def 9;
then A1: dom (freqSEQ s) = dom (FDprobSEQ s) by DIST_1:def 3;
for n being object st n in dom (freqSEQ s) holds
(freqSEQ s) . n = (len s) * ((FDprobSEQ s) . n) by DIST_1:def 9;
hence freqSEQ s = (len s) (#) (FDprobSEQ s) by A1, VALUED_1:def 5; :: thesis: verum