let E be 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
ex u being Element of E ^omega st
( w1 ^ u = w2 & v1 = u ^ v2 )
let v1, v2, w1, w2 be Element of E ^omega ; ( 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 )
; 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
; ( w1 ^ u = w2 & v1 = u ^ v2 )
thus
w1 ^ u = w2
by A3; v1 = u ^ v2
w2 ^ v2 = w1 ^ (u ^ v2)
by A3, AFINSQ_1:27;
hence
v1 = u ^ v2
by A1, AFINSQ_1:28; verum