let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for f being Element of NAT holds f <> NextLoc f,T
let T be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for f being Element of NAT holds f <> NextLoc f,T
let f be Element of NAT ; :: thesis: f <> NextLoc f,T
assume f = NextLoc f,T ; :: thesis: contradiction
then locnum f,T = (locnum f,T) + 1 by Def13;
hence contradiction ; :: thesis: verum