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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (i Shift p) or x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } )
assume x in dom (i Shift p) ; :: thesis: x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }
then consider k1 being Element of NAT such that
A3: x = i + k1 and
A4: k1 in dom p by A2;
consider k being Element of 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 Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } by A3, A5, A8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } or x in dom (i Shift p) )
assume x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } ; :: thesis: x in dom (i Shift p)
then consider j1 being Element of 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: k2 in NAT by ORDINAL1:def 12;
A14: 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, A14;
hence x in dom (i Shift p) by A2, A9, A12; :: thesis: verum