theorem Th54: :: MMLQUERY:54
for A being FinSequence
for a being set holds #occurrences (a,A) <= len A