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