let i be Element of NAT ; :: thesis: for p being FinSequence st p <> {} holds
dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }
let p be FinSequence; :: thesis: ( p <> {} implies dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } )
assume p <> {} ; :: 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 & k1 in dom p ) by A2;
consider k being Element of NAT such that
A4: ( k1 = k & 1 <= k & k <= len p ) by A1, A3;
( i + 1 <= i + k & i + k <= i + (len p) ) by A4, XREAL_1:9;
hence x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } by A3, A4; :: 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
A5: ( x = j1 & i + 1 <= j1 & j1 <= i + (len p) ) ;
i + 0 <= i + 1 by XREAL_1:9;
then consider k2 being Nat such that
A6: j1 = i + k2 by A5, NAT_1:10, XXREAL_0:2;
A7: k2 in NAT by ORDINAL1:def 13;
( 1 <= k2 & k2 <= len p ) by A5, A6, XREAL_1:8;
then k2 in dom p by A1, A7;
hence x in dom (i Shift p) by A2, A5, A6; :: thesis: verum