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 by A4, XBOOLE_0:def 4;
A6: x in dom (i Shift p2) by A4, XBOOLE_0:def 4;
A7: ex k1 being Element of NAT st
( x = k1 & 1 <= k1 & k1 <= len p1 ) by A2, A5;
consider k2 being Element of NAT such that
A8: x = i + k2 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;
Seg n = { m where m is Element of NAT : ( 1 <= m & m <= n ) } by FINSEQ_1:def 1;
then ex m being Element of NAT st
( k2 = m & 1 <= m & m <= n ) by A11;
then A12: 1 - 1 < k2 - 0 by XREAL_1:15;
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 (i Shift p2)) = {} by XBOOLE_0:def 1; :: according to XBOOLE_0:def 7 :: thesis: verum