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