for E being set
for S being semi-Thue-system of E
for t, u being Element of E ^omega
for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
(t ^+ p) +^ u is RedSequence of ==>.-relation S