:: deftheorem defines SCM-Chg SCMRING1:def 5 :
for R being non empty 1-sorted
for s being SCM-State of R
for u being natural Number holds SCM-Chg (s,u) = s +* (NAT .--> u);