let i be Nat; :: thesis: for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds
dom (Shift (q1,i)) misses dom (Shift (q2,i))
let q1, q2 be FinSubsequence; :: thesis: ( dom q1 misses dom q2 implies dom (Shift (q1,i)) misses dom (Shift (q2,i)) )
assume A1: dom q1 misses dom q2 ; :: thesis: dom (Shift (q1,i)) misses dom (Shift (q2,i))
A2: dom (Shift (q1,i)) = { (k + i) where k is Nat : k in dom q1 } by Def12;
A3: dom (Shift (q2,i)) = { (k + i) where k is Nat : k in dom q2 } by Def12;

now :: thesis: for x being object holds not x in (dom (Shift (q1,i))) /\ (dom (Shift (q2,i)))

given x being object such that A4: x in (dom (Shift (q1,i))) /\ (dom (Shift (q2,i))) ; :: thesis: contradiction
A5: x in dom (Shift (q1,i)) by A4, XBOOLE_0:def 4;
A6: x in dom (Shift (q2,i)) by A4, XBOOLE_0:def 4;
A7: ex k1 being Nat st
( x = k1 + i & k1 in dom q1 ) by A2, A5;
consider k2 being Nat such that
A8: x = k2 + i and
A9: k2 in dom q2 by A3, A6;
k2 in (dom q1) /\ (dom q2) by A7, A8, A9, XBOOLE_0:def 4;
hence contradiction by A1; :: thesis: verum

end;

hence (dom (Shift (q1,i))) /\ (dom (Shift (q2,i))) = {} by XBOOLE_0:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum