let il be Instruction-Location of SCM+FSA ; :: thesis: for dl being Int-Location holds il <> dl
let dl be Int-Location ; :: thesis: il <> dl
il in NAT by AMI_1:def 4;
then A: il is natural by ORDINAL1:def 13;
dl in SCM+FSA-Data-Loc by Def4;
then dl in [:{1},NAT :] ;
then ex x, y being set st
( x in {1} & y in NAT & dl = [x,y] ) by ZFMISC_1:103;
hence il <> dl ; :: thesis: verum