theorem :: MIDSP_3:3

for i being Nat
for D being non empty set
for c being Element of D
for p, q, r being FinSequence of D st p = (q ^ <*c*>) ^ r & i = (len q) + 1 holds
( ( for l being Nat st 1 <= l & l <= len q holds
p . l = q . l ) & p . i = c & ( for l being Nat st i + 1 <= l & l <= len p holds
p . l = r . (l - i) ) )