let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being FinPartState of S holds dom (Shift f,k) = { (il + k) where il is Instruction-Location of S : il in dom f }
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for f being FinPartState of S holds dom (Shift f,k) = { (il + k) where il is Instruction-Location of S : il in dom f }
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for f being FinPartState of S holds dom (Shift f,k) = { (il + k) where il is Instruction-Location of S : il in dom f }
let f be FinPartState of S; :: thesis: dom (Shift f,k) = { (il + k) where il is Instruction-Location of S : il in dom f }
A1: dom (Shift f,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom f } by Def16;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (il + k) where il is Instruction-Location of S : il in dom f } c= dom (Shift f,k)

let e be set ; :: thesis: ( e in dom (Shift f,k) implies e in { (il + k) where il is Instruction-Location of S : il in dom f } )
assume e in dom (Shift f,k) ; :: thesis: e in { (il + k) where il is Instruction-Location of S : il in dom f }
then consider m being Element of NAT such that
A2: e = il. S,(m + k) and
A3: il. S,m in dom f by A1;
(il. S,m) + k = il. S,((locnum (il. S,m)) + k)
.= il. S,(m + k) by AMISTD_1:def 13 ;
hence e in { (il + k) where il is Instruction-Location of S : il in dom f } by A2, A3; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (il + k) where il is Instruction-Location of S : il in dom f } or e in dom (Shift f,k) )
assume e in { (il + k) where il is Instruction-Location of S : il in dom f } ; :: thesis: e in dom (Shift f,k)
then consider il being Instruction-Location of S such that
A4: e = il + k and
A5: il in dom f ;
( il = il. S,(locnum il) & il + k = il. S,((locnum il) + k) ) by AMISTD_1:def 13;
hence e in dom (Shift f,k) by A1, A4, A5; :: thesis: verum