let N be with_zero set ; for T being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds
f = g
let T be non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N; for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds
f = g
let f, g be Element of NAT ; ( NextLoc (f,T) = NextLoc (g,T) implies f = g )
assume A1:
NextLoc (f,T) = NextLoc (g,T)
; f = g
set m = locnum (g,T);
set k = locnum (f,T);
(locnum (f,T)) + 0 =
((locnum (f,T)) + 1) - 1
.=
((locnum (g,T)) + 1) - 1
by A1, Th5
.=
(locnum (g,T)) + 0
;
hence
f = g
by Th7; verum