IC SCM = NAT by AMI_2:30, FUNCT_7:def 1;
then ObjectKind (IC SCM ) = NAT by AMI_2:def 5;
hence SCM is IC-Ins-separated by COMPOS_1:def 6; :: thesis: SCM is definite
let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of SCM . l = the Instructions of SCM
thus the Object-Kind of SCM . l = the Instructions of SCM by AMI_2:11; :: thesis: verum