let E be set ; :: thesis: for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds
s = t
let s, t be Element of E ^omega ; :: thesis: ( s ==>* t, {} ((E ^omega),(E ^omega)) implies s = t )
assume s ==>* t, {} ((E ^omega),(E ^omega)) ; :: thesis: s = t
then ==>.-relation ({} ((E ^omega),(E ^omega))) reduces s,t by Def7;
then {} ((E ^omega),(E ^omega)) reduces s,t by Th29;
then {} reduces s,t by PARTIT_2:def 1;
hence s = t by REWRITE1:13; :: thesis: verum