theorem :: AMI_WSTD:13

for z being Nat
for N being with_zero set
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 (locnum (f,T)) + z = locnum ((f + (z,T)),T) by Def5;