for p being XFinSequence
for i being Element of NAT
for x being set holds
( len (Replace (p,i,x)) = len p & ( i < len p implies (Replace (p,i,x)) . i = x ) & ( for j being Element of NAT st j <> i holds
(Replace (p,i,x)) . j = p . j ) )