let k, i be Element of NAT ; for q being FinSubsequence st dom q c= Seg k holds
dom (i Shift q) c= Seg (i + k)
let q be FinSubsequence; ( dom q c= Seg k implies dom (i Shift q) c= Seg (i + k) )
assume A1:
dom q c= Seg k
; dom (i Shift q) c= Seg (i + k)
A2:
dom (i Shift q) = { (i + j) where j is Element of NAT : j in dom q }
by Def15;
A3:
Seg k = { j where j is Element of NAT : ( 1 <= j & j <= k ) }
by FINSEQ_1:def 1;
A4:
Seg (i + k) = { j where j is Element of NAT : ( 1 <= j & j <= i + k ) }
by FINSEQ_1:def 1;
let x be set ; TARSKI:def 3 ( not x in dom (i Shift q) or x in Seg (i + k) )
assume
x in dom (i Shift q)
; x in Seg (i + k)
then consider j1 being Element of NAT such that
A5:
x = i + j1
and
A6:
j1 in dom q
by A2;
j1 in Seg k
by A1, A6;
then A7:
ex j2 being Element of NAT st
( j1 = j2 & 1 <= j2 & j2 <= k )
by A3;
0 <= i
by NAT_1:2;
then A8:
0 + 1 <= i + j1
by A7, XREAL_1:7;
i + j1 <= i + k
by A7, XREAL_1:7;
hence
x in Seg (i + k)
by A4, A5, A8; verum