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 COMPOS_1:def 8;
ObjectKind (IC SCM+FSA ) = NAT by COMPOS_1:def 6;
hence IC SCM+FSA <> l by A, SCMFSA_1:13; :: thesis: verum