let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s ==>* t,S holds
( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

let S be semi-Thue-system of E; :: thesis: for s, t, u being Element of E ^omega st s ==>* t,S holds
( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )

let s, t, u be Element of E ^omega ; :: thesis: ( s ==>* t,S implies ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) )
assume s ==>* t,S ; :: thesis: ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S )
then ==>.-relation S reduces s,t ;
then consider p being RedSequence of ==>.-relation S such that
A1: p . 1 = s and
A2: p . (len p) = t by REWRITE1:def 3;
reconsider p = p as FinSequence of E ^omega by ;
1 in dom p by FINSEQ_5:6;
then A3: (p +^ u) . 1 = s ^ u by ;
A4: len p = len (p +^ u) by Th5;
then len (p +^ u) in dom p by FINSEQ_5:6;
then A5: (p +^ u) . (len (p +^ u)) = t ^ u by A2, A4, Def3;
p +^ u is RedSequence of ==>.-relation S by Th23;
then ==>.-relation S reduces s ^ u,t ^ u by ;
hence s ^ u ==>* t ^ u,S ; :: thesis: u ^ s ==>* u ^ t,S
1 in dom p by FINSEQ_5:6;
then A6: (u ^+ p) . 1 = u ^ s by ;
A7: len p = len (u ^+ p) by Th5;
then len (u ^+ p) in dom p by FINSEQ_5:6;
then A8: (u ^+ p) . (len (u ^+ p)) = u ^ t by A2, A7, Def2;
u ^+ p is RedSequence of ==>.-relation S by Th23;
then ==>.-relation S reduces u ^ s,u ^ t by ;
hence u ^ s ==>* u ^ t,S ; :: thesis: verum