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