set X = { (k + i) where k is Nat : k in dom p } ;
set f = Shift (p,i);
consider K being Nat such that
A1: dom p c= Seg K by FINSEQ_1:def 12;
A2: dom (Shift (p,i)) = { (k + i) where k is Nat : k in dom p } by Def12;
{ (k + i) where k is Nat : k in dom p } c= Seg (i + K)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (k + i) where k is Nat : k in dom p } ; :: thesis:
then consider k being Nat such that
A3: x = k + i and
A4: k in dom p ;
A5: i + k >= k by NAT_1:11;
A6: k >= 1 by A1, A4, FINSEQ_1:1;
A7: k <= K by A1, A4, FINSEQ_1:1;
i + k >= 1 by A5, A6, XXREAL_0:2;
hence x in Seg (i + K) by A3, A7, FINSEQ_1:1, XREAL_1:6; :: thesis:

end;