for A being FinSequence holds max# A <= len A