theorem Th19: :: FINSEQ_4:19

for p being FinSequence
for x being object st x in rng p holds
p . (x .. p) = x