theorem :: SCMFSA_1:19

for s being SCM+FSA-State
for u being Nat holds (SCM+FSA-Chg (s,u)) . NAT = u