theorem :: DIST_1:4

for S being finite set

for s being FinSequence of S

for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))

for s being FinSequence of S

for x being set holds frequency (x,s) = (len s) * (FDprobability (x,s))