A1: dom (Shift F,k) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
thus rng (Shift F,k) c= X :: according to RELAT_1:def 19 :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Shift F,k) or x in X )
assume x in rng (Shift F,k) ; :: thesis: x in X
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 = m + k and
W4: m in dom F by W1, A1;
(Shift F,k) . (m + k) = F . m by W4, Def12
.= F /. m by W4, PARTFUN1:def 8 ;
hence x in X by W2, W3; :: thesis: verum

end;