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 :: thesis: for i being Nat st i in dom (p +^ u) & i + 1 in dom (p +^ u) holds
[((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S
let i be 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 ;
then A6: (p +^ u) . (i + 1) = (p . (i + 1)) ^ u by Def3;
A7: i in dom p by ;
then [(p . i),(p . (i + 1))] in ==>.-relation S by ;
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 ;
hence [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S by A6, A8, Def6; :: thesis: verum
end;
A9: now :: thesis: for i being Nat st i in dom (u ^+ p) & i + 1 in dom (u ^+ p) holds
[((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S
let i be 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 ;
then A13: (u ^+ p) . (i + 1) = u ^ (p . (i + 1)) by Def2;
A14: i in dom p by ;
then [(p . i),(p . (i + 1))] in ==>.-relation S by ;
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 ;
hence [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S by ; :: thesis: verum
end;
len (p +^ u) = len p by Th5;
hence p +^ u is RedSequence of ==>.-relation S by ; :: thesis: u ^+ p is RedSequence of ==>.-relation S
len (u ^+ p) = len p by Th5;
hence u ^+ p is RedSequence of ==>.-relation S by ; :: thesis: verum