let I be Program of SCM+FSA ; :: thesis: for a being Int-Location holds not a in dom I
let a be Int-Location ; :: thesis: not a in dom I
assume A1: a in dom I ; :: thesis: contradiction
dom I c= NAT by RELAT_1:def 18;
then reconsider a = a as Instruction-Location of SCM+FSA by A1, AMI_1:def 4;
a = a ;
hence contradiction by SCMFSA_2:84; :: thesis: verum