let s be State of SCM+FSA ; :: thesis: IC SCM+FSA in dom s
dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
then A1: {(IC SCM+FSA )} c= dom s by XBOOLE_1:7, XBOOLE_1:11;
IC SCM+FSA in {(IC SCM+FSA )} by TARSKI:def 1;
hence IC SCM+FSA in dom s by A1; :: thesis: verum