A1: dom (Shift (F,k)) = { (m + k) where m is Nat : m in dom F } by Def12;
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 object such that
A2: a in dom (Shift (F,k)) ;
ex m being Nat st
( a = m + k & m in dom F ) by A1, A2;
hence contradiction ; :: thesis: verum