let i be Nat; :: thesis: 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 ; :: thesis: for q being FinSubsequence st dom q c= Seg k holds
dom (Shift (q,i)) c= Seg (i + k)
let q be FinSubsequence; :: thesis: ( dom q c= Seg k implies dom (Shift (q,i)) c= Seg (i + k) )
assume A1: dom q c= Seg k ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (Shift (q,i)) or x in Seg (i + k) )
assume x in dom (Shift (q,i)) ; :: thesis: 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; :: thesis: verum