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