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

now

given x being set such that A4: x in (dom (i Shift q1)) /\ (dom (i Shift q2)) ; :: thesis: contradiction
A5: x in dom (i Shift q1) by A4, XBOOLE_0:def 4;
A6: x in dom (i Shift q2) by A4, XBOOLE_0:def 4;
A7: ex k1 being Element of NAT st
( x = i + k1 & k1 in dom q1 ) by A2, A5;
consider k2 being Element of NAT such that
A8: x = i + k2 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, XBOOLE_0:def 7; :: thesis: verum

end;

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