let E be non empty set ; :: thesis: for w1, v1, w2, v2 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 ) )
let w1, v1, w2, v2 be Element of E ^omega ; :: thesis: ( 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 ) )
assume A: w1 ^ v1 = w2 ^ v2 ; :: thesis: ( 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 ) )
( len w1 < len w2 or len w1 >= len w2 ) ;
hence ( 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 ) ) by A, LmXSeq66; :: thesis: verum