theorem Th6: :: FINSEQ_6:171

for D being non empty set
for p being Element of D
for f being FinSequence of D holds 1 <= len (f :- p)