let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S holds
(u ^ s) ^ v ==>* (u ^ t) ^ v,S
let S be semi-Thue-system of E; :: thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S holds
(u ^ s) ^ v ==>* (u ^ t) ^ v,S
let s, t, u, v be Element of E ^omega ; :: thesis: ( s ==>* t,S implies (u ^ s) ^ v ==>* (u ^ t) ^ v,S )
assume s ==>* t,S ; :: thesis: (u ^ s) ^ v ==>* (u ^ t) ^ v,S
then u ^ s ==>* u ^ t,S by Th36;
hence (u ^ s) ^ v ==>* (u ^ t) ^ v,S by Th36; :: thesis: verum