theorem :: AMI_WSTD:11

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 f + (0,T) = f by Def5;