let i be Nat; :: thesis: for p being FinSequence holds dom (Shift (p,i)) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }
let p be FinSequence; :: thesis: dom (Shift (p,i)) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }
A1: dom p = Seg (len p) by FINSEQ_1:def 3
.= { k where k is Nat : ( 1 <= k & k <= len p ) } ;
set X = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } ;
A2: dom (Shift (p,i)) = { (k1 + i) where k1 is Nat : k1 in dom p } by Def12;
thus dom (Shift (p,i)) c= { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } :: according to XBOOLE_0:def 10 :: thesis: { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } c= dom (Shift (p,i))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Shift (p,i)) or x in { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } )
assume x in dom (Shift (p,i)) ; :: thesis: x in { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }
then consider k1 being Nat such that
A3: x = k1 + i and
A4: k1 in dom p by A2;
consider k being Nat such that
A5: k1 = k and
A6: 1 <= k and
A7: k <= len p by A1, A4;
A8: i + 1 <= i + k by A6, XREAL_1:7;
i + k <= i + (len p) by A7, XREAL_1:7;
hence x in { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } by A3, A5, A8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } or x in dom (Shift (p,i)) )
assume x in { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } ; :: thesis: x in dom (Shift (p,i))
then consider j1 being Nat such that
A9: x = j1 and
A10: i + 1 <= j1 and
A11: j1 <= i + (len p) ;
i + 0 <= i + 1 by XREAL_1:7;
then consider k2 being Nat such that
A12: j1 = i + k2 by A10, NAT_1:10, XXREAL_0:2;
A13: 1 <= k2 by A10, A12, XREAL_1:6;
k2 <= len p by A11, A12, XREAL_1:6;
then k2 in dom p by A1, A13;
hence x in dom (Shift (p,i)) by A2, A9, A12; :: thesis: verum