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

for s being Element of E ^omega st s ==>. s,S holds

ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S )

let S be semi-Thue-system of E; :: thesis: for s being Element of E ^omega st s ==>. s,S holds

ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S )

let s be Element of E ^omega ; :: thesis: ( s ==>. s,S implies ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S ) )

given v, w, s1, t1 being Element of E ^omega such that A1: s = (v ^ s1) ^ w and

A2: s = (v ^ t1) ^ w and

A3: s1 -->. t1,S ; :: according to REWRITE2:def 5 :: thesis: ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S )

v ^ s1 = v ^ t1 by A1, A2, AFINSQ_1:28;

then s1 = t1 by AFINSQ_1:28;

hence ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S ) by A1, A3; :: thesis: verum

for s being Element of E ^omega st s ==>. s,S holds

ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S )

let S be semi-Thue-system of E; :: thesis: for s being Element of E ^omega st s ==>. s,S holds

ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S )

let s be Element of E ^omega ; :: thesis: ( s ==>. s,S implies ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S ) )

given v, w, s1, t1 being Element of E ^omega such that A1: s = (v ^ s1) ^ w and

A2: s = (v ^ t1) ^ w and

A3: s1 -->. t1,S ; :: according to REWRITE2:def 5 :: thesis: ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S )

v ^ s1 = v ^ t1 by A1, A2, AFINSQ_1:28;

then s1 = t1 by AFINSQ_1:28;

hence ex v, w, s1 being Element of E ^omega st

( s = (v ^ s1) ^ w & s1 -->. s1,S ) by A1, A3; :: thesis: verum