theorem :: FINSEQ_5:80

for D being non empty set
for f being FinSequence of D
for l1, l2 being Nat holds (f /^ l1) | (l2 -' l1) = (f | l2) /^ l1