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