theorem :: REWRITE2:38

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 & u ==>* v,S holds
( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S )