let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t being Element of E ^omega holds
( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega )) )
let S be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega holds
( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega )) )
let s, t be Element of E ^omega ; :: thesis: ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega )) )
thus ( s ==>* t,S implies s ==>* t,S \/ (id (E ^omega )) ) by Th40, XBOOLE_1:7; :: thesis: ( s ==>* t,S \/ (id (E ^omega )) implies s ==>* t,S )
assume s ==>* t,S \/ (id (E ^omega )) ; :: thesis: s ==>* t,S
then ==>.-relation (S \/ (id (E ^omega ))) reduces s,t by Def7;
then (==>.-relation S) \/ (id (E ^omega )) reduces s,t by Th28;
then ==>.-relation S reduces s,t by REWRITE1:24;
hence s ==>* t,S by Def7; :: thesis: verum