A1: dom [:NAT ,(((union {the carrier of R}) \/ SCM-Memory ) * ):] = NAT by SYSREL:12;
SCM-Instr R c= [:NAT ,(((union {the carrier of R}) \/ SCM-Memory ) * ):] ;
then the Instructions of (SCM R) c= [:NAT ,(((union {the carrier of R}) \/ SCM-Memory ) * ):] by SCMRING2:def 1;
then A2: dom the Instructions of (SCM R) c= NAT by A1, RELAT_1:25;
InsCode I in dom the Instructions of (SCM R) ;
hence InsCode I is natural by A2; :: thesis: verum