let s be State of SCM+FSA ; :: thesis: for l being Element of NAT holds l in dom s
let l be Element of NAT ; :: 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 ;
hence l in dom s by A1; :: thesis: verum