theorem :: AMI_2:11

for s being SCM-State
for u being natural Number holds (SCM-Chg (s,u)) . NAT = u