let E be non empty set ; :: thesis: for w1, v1, w2, v2 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 w1, v1, w2, v2 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 )
A3: (len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:20
.= (len w2) + (len v2) by AFINSQ_1:20 ;
( len v1 >= len v2 implies ((len w1) + (len v1)) - (len v1) <= ((len w2) + (len v2)) - (len v2) ) by A3, XREAL_1:15;
then consider u' being XFinSequence such that
B: w1 ^ u' = w2 by A1, A2, AFINSQ_1:45;
reconsider u = u' as Element of E ^omega by B, FLANG_1:5;
take u ; :: thesis: ( w1 ^ u = w2 & v1 = u ^ v2 )
thus w1 ^ u = w2 by B; :: thesis: v1 = u ^ v2
w2 ^ v2 = w1 ^ (u ^ v2) by B, AFINSQ_1:30;
hence v1 = u ^ v2 by A1, AFINSQ_1:31; :: thesis: verum