let s be State of SCM+FSA; :: thesis: for s9 being State of SCM holds (s +* s9) +* (s | NAT) is State of SCM+FSA
let s9 be State of SCM; :: thesis: (s +* s9) +* (s | NAT) is State of SCM+FSA
reconsider s = s as SCM+FSA-State by PBOOLE:155;
reconsider s9 = s9 as SCM-State by PBOOLE:155;
(s +* s9) +* (s | NAT) is State of SCM+FSA by SCMFSA_1:19;
hence (s +* s9) +* (s | NAT) is State of SCM+FSA ; :: thesis: verum