let E be set ; :: thesis: for S being semi-Thue-system of E

for t, u being Element of E ^omega

for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds

(t ^+ p) +^ u is RedSequence of ==>.-relation S

let S be semi-Thue-system of E; :: thesis: for t, u being Element of E ^omega

for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds

(t ^+ p) +^ u is RedSequence of ==>.-relation S

let t, u be Element of E ^omega ; :: thesis: for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds

(t ^+ p) +^ u is RedSequence of ==>.-relation S

let p be FinSequence of E ^omega ; :: thesis: ( p is RedSequence of ==>.-relation S implies (t ^+ p) +^ u is RedSequence of ==>.-relation S )

assume p is RedSequence of ==>.-relation S ; :: thesis: (t ^+ p) +^ u is RedSequence of ==>.-relation S

then t ^+ p is RedSequence of ==>.-relation S by Th23;

hence (t ^+ p) +^ u is RedSequence of ==>.-relation S by Th23; :: thesis: verum

for t, u being Element of E ^omega

for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds

(t ^+ p) +^ u is RedSequence of ==>.-relation S

let S be semi-Thue-system of E; :: thesis: for t, u being Element of E ^omega

for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds

(t ^+ p) +^ u is RedSequence of ==>.-relation S

let t, u be Element of E ^omega ; :: thesis: for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds

(t ^+ p) +^ u is RedSequence of ==>.-relation S

let p be FinSequence of E ^omega ; :: thesis: ( p is RedSequence of ==>.-relation S implies (t ^+ p) +^ u is RedSequence of ==>.-relation S )

assume p is RedSequence of ==>.-relation S ; :: thesis: (t ^+ p) +^ u is RedSequence of ==>.-relation S

then t ^+ p is RedSequence of ==>.-relation S by Th23;

hence (t ^+ p) +^ u is RedSequence of ==>.-relation S by Th23; :: thesis: verum