theorem :: FINSEQ_4:70

for a, m being Nat
for D being set
for p being FinSequence of D st a in dom (p | m) holds
(p | m) /. a = p /. a