let A be FinSequence; :: thesis: max# A <= len A
for a being set holds #occurrences (a,A) <= len A by Th21;
hence max# A <= len A by MAX; :: thesis: verum