theorem Th8: :: SCMFSA_1:18

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