let s be State of SCM+FSA; :: thesis: for s9 being State of SCM holds s +* s9 is State of SCM+FSA
let s9 be State of SCM; :: thesis: s +* s9 is State of SCM+FSA
reconsider s = s as SCM+FSA-State by CARD_3:107;
reconsider s9 = s9 as SCM-State by CARD_3:107;
s +* s9 is SCM+FSA-State by SCMFSA_1:18;
then s +* s9 is State of SCM+FSA ;
hence s +* s9 is State of SCM+FSA ; :: thesis: verum