let s be State of SCM+FSA ; :: thesis: for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT )
let x be set ; :: thesis: ( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT )
assume A1: x in dom s ; :: thesis: ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT )
dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by PARTFUN1:def 4, SCMFSA_2:8;
then ( x in (Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )} or x in NAT ) by A1, XBOOLE_0:def 3;
then ( x in Int-Locations \/ FinSeq-Locations or x in {(IC SCM+FSA )} or x in NAT ) by XBOOLE_0:def 3;
then ( x in Int-Locations or x in FinSeq-Locations or x = IC SCM+FSA or x is Element of NAT ) by TARSKI:def 1, XBOOLE_0:def 3;
hence ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT ) by SCMFSA_2:11, SCMFSA_2:12; :: thesis: verum