let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i being Nat holds rng (Replace f,i,p) c= (rng f) \/ {p}
let f be FinSequence of D; :: thesis: for p being Element of D
for i being Nat holds rng (Replace f,i,p) c= (rng f) \/ {p}
let p be Element of D; :: thesis: for i being Nat holds rng (Replace f,i,p) c= (rng f) \/ {p}
let i be Nat; :: thesis: rng (Replace f,i,p) c= (rng f) \/ {p}
reconsider i = i as Element of NAT by ORDINAL1:def 13;
rng <*p*> = {p}
by FINSEQ_1:56;
then A1:
(rng f) \/ {p} = rng (f ^ <*p*>)
by FINSEQ_1:44;
set P = f | (i -' 1);
set Q = f /^ i;
set F = <*(f . i)*>;