theorem Th20: :: FINSEQ_4:20

for p being FinSequence
for x being object st x in rng p holds
x .. p in dom p