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 l being Instruction-Location of S holds (l + k) -' k = l
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 l being Instruction-Location of S holds (l + k) -' k = l
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l being Instruction-Location of S holds (l + k) -' k = l
let l be Instruction-Location of S; :: thesis: (l + k) -' k = l
thus (l + k) -' k = il. S,(((locnum l) + k) -' k) by Def13
.= il. S,(locnum l) by NAT_D:34
.= l by Def13 ; :: thesis: verum