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:23;
hence s ==>* t,S by Def7; :: thesis: verum