theorem :: SCMFSA_2:50

for s being State of SCM+FSA
for s9 being State of SCM holds s +* s9 is State of SCM+FSA