let N be with_zero set ; :: thesis: for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f being Element of NAT holds f <> NextLoc (f,T)
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over 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 Def5;
hence contradiction ; :: thesis: verum