theorem Th61: :: FINSEQ_6:61

for D being non empty set
for p being Element of D
for f being FinSequence of D holds p in rng (f :- p)