for m, n being Nat
for L being non empty ZeroStr
for p being sequence of L st m <> n holds
(p || n) . m = p . m by FUNCT_7:32;