let s be State of ; :: thesis: for l being Instruction-Location of SCM+FSA holds l in dom s
let l be Instruction-Location of SCM+FSA ; :: thesis: l in dom s
dom s = ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT by SCMFSA6A:34;
then A1: NAT c= dom s by XBOOLE_1:7;
l in NAT by AMI_1:def 4;
hence l in dom s by A1; :: thesis: verum