A1: dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F } by Def16;
thus rng (Shift F,k) c= the Instructions of S :: according to RELAT_1:def 19 :: thesis: Shift F,k is NAT -defined

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Shift F,k) or x in the Instructions of S )
assume x in rng (Shift F,k) ; :: thesis: x in the Instructions of S
then consider y being set such that
W1: y in dom (Shift F,k) and
W2: x = (Shift F,k) . y by FUNCT_1:def 5;
consider m being Element of NAT such that
W3: y = il. S,(m + k) and
W4: il. S,m in dom F by W1, A1;
(Shift F,k) . (il. S,(m + k)) = F . (il. S,m) by W4, Def16
.= F /. (il. S,m) by W4, PARTFUN1:def 8 ;
hence x in the Instructions of S by W2, W3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not x in proj1 (Shift F,k) or x in NAT )
assume x in dom (Shift F,k) ; :: thesis: x in NAT
then ex m being Element of NAT st
( x = il. S,(m + k) & il. S,m in dom F ) by A1;
hence x in NAT ; :: thesis: verum