let l be Instruction-Location of SCM+FSA ; :: thesis: IC SCM+FSA <> l
ObjectKind l = the Instructions of SCM+FSA by AMI_1:def 14;
hence IC SCM+FSA <> l by AMI_1:def 11, SCMFSA_1:13; :: thesis: verum