theorem :: FINSEQ_7:6

for f being FinSequence
for i being Nat
for p being set holds rng (Replace (f,i,p)) c= (rng f) \/ {p} by FUNCT_7:100;