theorem Th23: :: FINSEQ_4:23

for p being FinSequence
for x being object st x in rng p holds
x .. p in p " {x}