theorem Th53: :: VALUED_1:54

for i being Nat
for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds
dom (Shift (q1,i)) misses dom (Shift (q2,i))