let il be Instruction-Location of SCM+FSA ; :: thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; :: thesis: il <> dl
A: il in NAT by AMI_1:def 4;
dl in SCM+FSA-Data*-Loc by Def5;
then B: dl in INT \ NAT by SCMFSA_1:def 1;
NAT misses INT \ NAT by XBOOLE_1:79;
hence il <> dl by A, B, XBOOLE_0:3; :: thesis: verum