let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, u being Element of E ^omega st s ==>. t,S holds
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let S be semi-Thue-system of E; :: thesis: for s, t, u being Element of E ^omega st s ==>. t,S holds
( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
let s, t, u be Element of E ^omega ; :: thesis: ( s ==>. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) )
given v, w, s1, t1 being Element of E ^omega such that A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w & s1 -->. t1,S ) ; :: according to REWRITE2:def 5 :: thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )
A2: u ^ s = (u ^ (v ^ s1)) ^ w by A1, AFINSQ_1:30
.= ((u ^ v) ^ s1) ^ w by AFINSQ_1:30 ;
u ^ t = (u ^ (v ^ t1)) ^ w by A1, AFINSQ_1:30
.= ((u ^ v) ^ t1) ^ w by AFINSQ_1:30 ;
hence u ^ s ==>. u ^ t,S by A1, A2, Def5; :: thesis: s ^ u ==>. t ^ u,S
A3: s ^ u = (v ^ s1) ^ (w ^ u) by A1, AFINSQ_1:30;
t ^ u = (v ^ t1) ^ (w ^ u) by A1, AFINSQ_1:30;
hence s ^ u ==>. t ^ u,S by A1, A3, Def5; :: thesis: verum