thus ObjectKind (IC (SCM R)) = (SCM-OK R) . (IC (SCM R)) by Def1
.= (SCM-OK R) . NAT by Def1
.= NAT by AMI_2:30, SCMRING1:def 3 ; :: according to AMI_1:def 11 :: thesis: verum