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, 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; :: thesis: for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds
f = g
let f, g be Element of NAT ; :: thesis: ( NextLoc (f,T) = NextLoc (g,T) implies f = g )
assume A1: NextLoc (f,T) = NextLoc (g,T) ; :: thesis: 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; :: thesis: verum