for A being FinSequence
for a being set st #occurrences (a,A) = len A holds
max# A = len A