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 OPOSET_1:def 1;
hence s = t by REWRITE1:14; :: thesis: verum