A1: dom (Shift (F,k)) = { (m + k) where m is Nat : m in dom F } by Def12;
consider a being object such that
A2: a in dom F by XBOOLE_0:def 1;
reconsider a = a as Element of NAT by A2;
consider m being Nat such that
A3: a = m ;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
m + k in dom (Shift (F,k)) by A1, A2, A3;
hence not Shift (F,k) is empty ; :: thesis: verum