theorem :: FINSEQ_3:106

for i being Nat
for p being FinSequence holds rng (Del (p,i)) c= rng p by FUNCT_1:14;