A1: dom (Shift (F,k)) = { (m + k) where m is 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 object ; :: 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 object such that
A2: y in dom (Shift (F,k)) and
A3: x = (Shift (F,k)) . y by FUNCT_1:def 3;
consider m being Nat such that
A4: y = m + k and
A5: m in dom F by A2, A1;
(Shift (F,k)) . (m + k) = F . m by A5, Def12
.= F /. m by A5, PARTFUN1:def 6 ;
hence x in X by A3, A4; :: thesis: verum

end;