let s be State of SCMPDS ; :: thesis: for l being Instruction-Location of SCMPDS holds l in dom s
let l be Instruction-Location of SCMPDS ; :: thesis: l in dom s
l in NAT by AMI_1:def 4;
then l in ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by XBOOLE_0:def 3;
hence l in dom s by AMI_1:79, SCMPDS_3:5; :: thesis: verum