JumpPart (halt SCM) is empty by LmX, RECDEF_2:def 2;
then halt SCM is ins-loc-free by COMPOS_1:def 37;
hence SCM is proper-halt by COMPOS_1:def 39; :: thesis: ( SCM is IC-Ins-separated & SCM is definite )
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