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