theorem :: REWRITE3:11

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
( w1 = w2 & v1 = v2 )