let E be non empty set ; :: thesis: 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 )
let v1, v2, w1, w2 be Element of E ^omega ; :: thesis: ( w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) implies ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 ) )
assume that
A1: w1 ^ v1 = w2 ^ v2 and
A2: ( len w1 <= len w2 or len v1 >= len v2 ) ; :: thesis: ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 )
(len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:17
.= (len w2) + (len v2) by AFINSQ_1:17 ;
then ( len v1 >= len v2 implies ((len w1) + (len v1)) - (len v1) <= ((len w2) + (len v2)) - (len v2) ) by XREAL_1:13;
then consider u9 being XFinSequence such that
A3: w1 ^ u9 = w2 by A1, A2, AFINSQ_1:41;
reconsider u = u9 as Element of E ^omega by A3, FLANG_1:5;
take u ; :: thesis: ( w1 ^ u = w2 & v1 = u ^ v2 )
thus w1 ^ u = w2 by A3; :: thesis: v1 = u ^ v2
w2 ^ v2 = w1 ^ (u ^ v2) by A3, AFINSQ_1:27;
hence v1 = u ^ v2 by A1, AFINSQ_1:28; :: thesis: verum