theorem Th42: :: FINSEQ_4:42

for p being FinSequence
for x being object
for n being Nat st x in rng p & n = (len p) - (x .. p) holds
dom (p |-- x) = Seg n