let N be with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for l1, l2 being Instruction-Location of T st locnum l1 = locnum l2 holds
l1 = l2
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for l1, l2 being Instruction-Location of T st locnum l1 = locnum l2 holds
l1 = l2
let l1, l2 be Instruction-Location of T; :: thesis: ( locnum l1 = locnum l2 implies l1 = l2 )
assume A1: locnum l1 = locnum l2 ; :: thesis: l1 = l2
( il. T,(locnum l1) = l1 & il. T,(locnum l2) = l2 ) by Def13;
hence l1 = l2 by A1; :: thesis: verum