for s being SCM+FSA-State
for s1 being SCM-State holds s +* s1 is SCM+FSA-State