for S being non empty finite set
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 )