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 by Def7;
then consider p being RedSequence of ==>.-relation S such that
A1: ( p . 1 = s & p . (len p) = t ) by REWRITE1:def 3;
reconsider p = p as FinSequence of E ^omega by A1, ABCMIZ_0:74;
A2: p +^ u is RedSequence of ==>.-relation S by Th23;
( (p +^ u) . 1 = s ^ u & (p +^ u) . (len (p +^ u)) = t ^ u )

proof

1 in dom p by FINSEQ_5:6;
hence (p +^ u) . 1 = s ^ u by A1, Def3; :: thesis: (p +^ u) . (len (p +^ u)) = t ^ u
A3: len p = len (p +^ u) by Th5;
then len (p +^ u) in dom p by FINSEQ_5:6;
hence (p +^ u) . (len (p +^ u)) = t ^ u by A1, A3, Def3; :: thesis: verum

end;

then ==>.-relation S reduces s ^ u,t ^ u by A2, REWRITE1:def 3;
hence s ^ u ==>* t ^ u,S by Def7; :: thesis: u ^ s ==>* u ^ t,S
A4: u ^+ p is RedSequence of ==>.-relation S by Th23;
( (u ^+ p) . 1 = u ^ s & (u ^+ p) . (len (u ^+ p)) = u ^ t )

proof

1 in dom p by FINSEQ_5:6;
hence (u ^+ p) . 1 = u ^ s by A1, Def2; :: thesis: (u ^+ p) . (len (u ^+ p)) = u ^ t
A5: len p = len (u ^+ p) by Th5;
then len (u ^+ p) in dom p by FINSEQ_5:6;
hence (u ^+ p) . (len (u ^+ p)) = u ^ t by A1, A5, Def2; :: thesis: verum

end;

then ==>.-relation S reduces u ^ s,u ^ t by A4, REWRITE1:def 3;
hence u ^ s ==>* u ^ t,S by Def7; :: thesis: verum