A1: dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F } by Def16;
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 Instruction-Location of S by A2, AMI_1:def 4;
consider m being natural number such that
A3: a = il. S,m by AMISTD_1:26;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
il. S,(m + k) in dom (Shift F,k) by A1, A2, A3;
hence not Shift F,k is empty ; :: thesis: verum