let N be non empty with_non-empty_elements set ; :: thesis: for T being non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of N
for f, g being Element of NAT st NextLoc (f,T) = NextLoc (g,T) holds
f = g
let T be non empty stored-program IC-Ins-separated definite weakly_standard AMI-Struct of 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, Th25
.= (locnum (g,T)) + 0 ;
hence f = g by Th27; :: thesis: verum