theorem Th70: :: FINSEQ_5:70

for n being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D holds rng (Ins (f,n,p)) = {p} \/ (rng f)