theorem :: FINSEQ_5:35

for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f holds
f |-- p = f /^ (p .. f)