let E be set ; :: thesis: for S being semi-Thue-system of E
for u being Element of E ^omega
for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S )
let S be semi-Thue-system of E; :: thesis: for u being Element of E ^omega
for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S )
let u be Element of E ^omega ; :: thesis: for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds
( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S )
let p be FinSequence of E ^omega ; :: thesis: ( p is RedSequence of ==>.-relation S implies ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) )
assume A1: p is RedSequence of ==>.-relation S ; :: thesis: ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S )

A2: now

let i be Element of NAT ; :: thesis: ( i in dom (p +^ u) & i + 1 in dom (p +^ u) implies [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S )
assume that
A3: i in dom (p +^ u) and
A4: i + 1 in dom (p +^ u) ; :: thesis: [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S
A5: i + 1 in dom p by A4, Def3;
then A6: (p +^ u) . (i + 1) = (p . (i + 1)) ^ u by Def3;
A7: i in dom p by A3, Def3;
then [(p . i),(p . (i + 1))] in ==>.-relation S by A1, A5, REWRITE1:def 2;
then p . i ==>. p . (i + 1),S by Def6;
then A8: (p . i) ^ u ==>. (p . (i + 1)) ^ u,S by Th12;
(p +^ u) . i = (p . i) ^ u by A7, Def3;
hence [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S by A6, A8, Def6; :: thesis: verum

end;

A9: now

let i be Element of NAT ; :: thesis: ( i in dom (u ^+ p) & i + 1 in dom (u ^+ p) implies [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S )
assume that
A10: i in dom (u ^+ p) and
A11: i + 1 in dom (u ^+ p) ; :: thesis: [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S
A12: i + 1 in dom p by A11, Def2;
then A13: (u ^+ p) . (i + 1) = u ^ (p . (i + 1)) by Def2;
A14: i in dom p by A10, Def2;
then [(p . i),(p . (i + 1))] in ==>.-relation S by A1, A12, REWRITE1:def 2;
then p . i ==>. p . (i + 1),S by Def6;
then A15: u ^ (p . i) ==>. u ^ (p . (i + 1)),S by Th12;
(u ^+ p) . i = u ^ (p . i) by A14, Def2;
hence [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S by A13, A15, Def6; :: thesis: verum

end;

len (p +^ u) = len p by Th5;
hence p +^ u is RedSequence of ==>.-relation S by A1, A2, REWRITE1:def 2; :: thesis: u ^+ p is RedSequence of ==>.-relation S
len (u ^+ p) = len p by Th5;
hence u ^+ p is RedSequence of ==>.-relation S by A1, A9, REWRITE1:def 2; :: thesis: verum