theorem :: SCMFSA_1:20

for s being SCM+FSA-State
for u being Nat
for mk being Element of SCM+FSA-Data-Loc holds (SCM+FSA-Chg (s,u)) . mk = s . mk