let i be Nat; :: thesis: for p1 being FinSequence
for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (Shift (p2,i))
let p1 be FinSequence; :: thesis: for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (Shift (p2,i))
let p2 be FinSubsequence; :: thesis: ( len p1 <= i implies dom p1 misses dom (Shift (p2,i)) )
assume A1: len p1 <= i ; :: thesis: dom p1 misses dom (Shift (p2,i))
A2: dom p1 = Seg (len p1) by FINSEQ_1:def 3
.= { k where k is Nat : ( 1 <= k & k <= len p1 ) } ;
A3: dom (Shift (p2,i)) = { (k + i) where k is Nat : k in dom p2 } by Def12;
for x being object holds not x in (dom p1) /\ (dom (Shift (p2,i)))

proof

given x being object such that A4: x in (dom p1) /\ (dom (Shift (p2,i))) ; :: thesis: contradiction
A5: x in dom p1 by A4, XBOOLE_0:def 4;
A6: x in dom (Shift (p2,i)) by A4, XBOOLE_0:def 4;
A7: ex k1 being Nat st
( x = k1 & 1 <= k1 & k1 <= len p1 ) by A2, A5;
consider k2 being Nat such that
A8: x = k2 + i and
A9: k2 in dom p2 by A3, A6;
consider n being Nat such that
A10: dom p2 c= Seg n by FINSEQ_1:def 12;
A11: k2 in Seg n by A9, A10;
A12: ex m being Nat st
( k2 = m & 1 <= m & m <= n ) by A11;
reconsider x = x as Element of NAT by A4;
(len p1) + k2 <= i + k2 by A1, XREAL_1:7;
then ((len p1) + k2) - k2 < x - 0 by A8, A12, XREAL_1:15;
hence contradiction by A7; :: thesis: verum

end;

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