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