let i be Nat; 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; ( dom q1 misses dom q2 implies dom (Shift (q1,i)) misses dom (Shift (q2,i)) )
assume A1:
dom q1 misses dom q2
; 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 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)))
;
contradictionA5:
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;
verum end;
hence
(dom (Shift (q1,i))) /\ (dom (Shift (q2,i))) = {}
by XBOOLE_0:def 1; XBOOLE_0:def 7 verum