theorem Th3: :: MATRIXJ1:3

for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom g holds
Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i))