theorem :: VALUED_1:55

for i being Nat
for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(Shift (q1,i)) \/ (Shift (q2,i)) = Shift (q,i)