A1: dom (Shift (F,k)) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
consider a being set such that
A2: a in dom F by XBOOLE_0:def 1;
dom F c= NAT by RELAT_1:def 18;
then reconsider a = a as Element of NAT by A2;
consider m being natural number such that
A3: a = m ;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
m + k in dom (Shift (F,k)) by A1, A2, A3;
hence not Shift (F,k) is empty ; :: thesis: verum