theorem Th58: :: FINSEQ_3:60

for p being FinSequence
for A being set holds len (p - A) <= len p