let l be Element of NAT ; :: thesis: IC SCM+FSA <> l
A: the Object-Kind of SCM+FSA . l = the Instructions of SCM+FSA by AMI_1:def 14;
ObjectKind (IC SCM+FSA ) = NAT by AMI_1:def 11;
hence IC SCM+FSA <> l by A, SCMFSA_1:13; :: thesis: verum