for s being SCM-State
for u being natural Number
for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk