theorem Th42: :: REWRITE2:42

for E being set
for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds
s = t