let i be Nat; 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; 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) ) }
XBOOLE_0:def 10 { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) } c= dom (Shift (p,i))
let x be object ; TARSKI:def 3 ( 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) ) }
; 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; verum