let aa be Int-Location; :: thesis: not Stop SCM+FSA refers aa
A1: rng (Stop SCM+FSA) = {(halt SCM+FSA)} by AFINSQ_1:33;
let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def 2 :: thesis: ( not i in rng (Stop SCM+FSA) or not i refers aa )
assume i in rng (Stop SCM+FSA) ; :: thesis: not i refers aa
then i = halt SCM+FSA by A1, TARSKI:def 1;
hence not i refers aa ; :: thesis: verum