:: deftheorem defines SCM+FSA-Chg SCMFSA_1:def 6 :
for s being SCM+FSA-State
for u being Nat holds SCM+FSA-Chg (s,u) = s +* (NAT .--> u);