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