theorem :: REWRITE2:15

for E being set
for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s -->. t,S holds
(u ^ s) ^ v ==>. (u ^ t) ^ v,S ;