theorem :: SCMFSA_M:30

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
s . (intloc 0) = 1