theorem :: SETWOP_2:23

for D being non empty set
for d being Element of D
for p being FinSequence of D holds rng ([#] (p,d)) = (rng p) \/ {d}