A1: dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F } by Def16;
assume not Shift F,k is empty ; :: thesis: contradiction
then reconsider f = Shift F,k as non empty Function ;
not dom f is empty ;
then consider a being set such that
A2: a in dom (Shift F,k) by XBOOLE_0:def 1;
ex m being Element of NAT st
( a = il. S,(m + k) & il. S,m in dom F ) by A1, A2;
hence contradiction ; :: thesis: verum