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

proof

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

end;

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