theorem Th13: :: REWRITE3:13

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