theorem Th12: :: REWRITE3:12

for E being non empty set
for v1, v2, w1, w2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) holds
ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 )