let z be natural number ; :: thesis: for N being with_non-empty_elements set
for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for f, g being Instruction-Location of T st f + z = g + z holds
f = g
let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for f, g being Instruction-Location of T st f + z = g + z holds
f = g
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for f, g being Instruction-Location of T st f + z = g + z holds
f = g
let f, g be Instruction-Location of T; :: thesis: ( f + z = g + z implies f = g )
assume f + z = g + z ; :: thesis: f = g
then (locnum f) + z = (locnum g) + z by Th25;
hence f = g by Th27; :: thesis: verum