theorem :: SCMFSA_1:21

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