theorem :: FINSEQ_5:24

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