let E be non empty set ; :: thesis: 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 ) )
let v1, v2, w1, w2 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 ) )
A1: ( len w1 < len w2 or len w1 >= len w2 ) ;
assume 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 ) )
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 A1, Th12; :: thesis: verum